Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-17 16:30 508b13ee

View on Github →

chore(*): flip various subsingleton_iff, nontrivial_iff lemmas and add simp (#8703)

Estimated changes

modified theorem subgroup.nontrivial_iff
modified theorem subgroup.subsingleton_iff
modified theorem submonoid.nontrivial_iff
modified theorem submonoid.subsingleton_iff
modified theorem submodule.nontrivial_iff
modified theorem submodule.subsingleton_iff