Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-04 21:12 fa204820

View on Github →

feat(linear_algebra/basic): add minor lemmas, tweak simp attributes (#11822)

Estimated changes

Modified src/algebra/module/submodule.lean

modified theorem submodule.coe_subtype

modified theorem submodule.subtype_apply

Modified src/linear_algebra/basic.lean

modified theorem submodule.comap_id

added theorem submodule.map_subtype_range_of_le

added theorem submodule.map_subtype_span_singleton

modified theorem submodule.span_singleton_le_iff_mem