Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-12 16:10 73ba4602

View on Github →

feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.nontrivial_iff

added theorem subgroup.subsingleton_iff

Modified src/group_theory/submonoid/basic.lean

added theorem submonoid.nontrivial_iff

added theorem submonoid.subsingleton_iff

Modified src/order/bounded_lattice.lean

added theorem subsingleton_iff_bot_eq_top