Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 18:19 f45dee43

View on Github →

feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641)

Estimated changes

Modified src/algebra/algebra/operations.lean

added theorem submodule.mem_span_mul_finite_of_mem_mul

added theorem submodule.mem_span_mul_finite_of_mem_span_mul

Modified src/algebra/pointwise.lean

added theorem finset.subset_mul

Modified src/linear_algebra/basic.lean

added theorem submodule.mem_span_finite_of_mem_span

Modified src/ring_theory/ideal/basic.lean

added theorem ring.ne_bot_of_is_maximal_of_not_is_field