Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 14:12 aa730c63

View on Github →

feat(linear_algebra): a module has a unique submodule iff it has a unique element (#6281) Also strengthens the related lemmas about subgroup and submonoid

Estimated changes

Modified src/group_theory/subgroup.lean

Modified src/group_theory/submonoid/basic.lean

Modified src/linear_algebra/basic.lean

deleted theorem submodule.bot_ne_top

added theorem submodule.bot_to_add_submonoid

deleted theorem submodule.eq_bot_of_zero_eq_one

added theorem submodule.nontrivial_iff

added theorem submodule.subsingleton_iff

added theorem submodule.top_to_add_submonoid

Modified src/linear_algebra/basis.lean

modified theorem is_basis_empty

deleted theorem is_basis_empty_bot

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/invariant_basis_number.lean

Modified src/ring_theory/ideal/basic.lean

Modified src/ring_theory/ideal/over.lean