Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-01 15:38 9b000466

View on Github →

chore(algebra,group_theory,right_theory,linear_algebra): add missing lemmas (#8948) This adds:

sub{group,ring,semiring}.map_id
submodule.add_mem_sup
submodule.map_add_le And moves submodule.sum_mem_supr and submodule.sum_mem_bsupr to an earlier file.

Estimated changes

Modified src/algebra/module/submodule_lattice.lean

added theorem submodule.add_mem_sup

added theorem submodule.sum_mem_bsupr

added theorem submodule.sum_mem_supr

Modified src/group_theory/subgroup.lean

added theorem subgroup.map_id

Modified src/linear_algebra/basic.lean

added theorem submodule.map_add_le

deleted theorem submodule.sum_mem_bsupr

deleted theorem submodule.sum_mem_supr

Modified src/ring_theory/subring.lean

added theorem subring.map_id

Modified src/ring_theory/subsemiring.lean

added theorem subsemiring.map_id