Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-01 14:39 8b69a4b2

View on Github →

feat(ring_theory): Some missing lemmas (#15064)

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

Modified src/linear_algebra/span.lean

added theorem submodule.closure_le_to_add_submonoid_span

added theorem submodule.closure_subset_span

added theorem submodule.span_closure

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_span

Modified src/ring_theory/finiteness.lean

added theorem algebra.finite_type.is_noetherian_ring

added theorem subalgebra.fg_iff_finite_type

Modified src/ring_theory/ideal/operations.lean

added theorem submodule.smul_inf_le

Modified src/ring_theory/noetherian.lean

added theorem submodule.fg_bsupr

added theorem submodule.fg_finset_sup

added theorem submodule.fg_supr