Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-08 11:43 e44aa6e7

View on Github →

feat(linear_algebra/basic): some lemmas about span and restrict_scalars (#10167)

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem submodule.span_le_restrict_scalars

Modified src/algebra/module/submodule.lean

added theorem submodule.coe_restrict_scalars

modified theorem submodule.restrict_scalars_mem

added theorem submodule.restrict_scalars_self

Modified src/linear_algebra/basic.lean

added theorem submodule.span_coe_eq_restrict_scalars

modified theorem submodule.span_eq

added theorem submodule.span_le_restrict_scalars

added theorem submodule.span_span_of_tower

added theorem submodule.span_subset_span

Modified src/linear_algebra/finsupp.lean

Modified src/linear_algebra/pi.lean

Modified src/ring_theory/finiteness.lean