Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-09 11:19 98895022

View on Github →

feat(linear_algebra/pi): add submodule.pi (#6576)

Estimated changes

Modified src/data/set/basic.lean

Modified src/linear_algebra/basic.lean

added theorem submodule.coe_subset_coe

added theorem submodule.sum_mem_bsupr

added theorem submodule.sum_mem_supr

Modified src/linear_algebra/pi.lean

added theorem submodule.binfi_comap_proj

added theorem submodule.coe_pi

added theorem submodule.infi_comap_proj

added theorem submodule.mem_pi

added def submodule.pi

added theorem submodule.supr_map_single

Modified src/linear_algebra/prod.lean