feat(group_theory/subgroup): eq_bot_of_card_eq (#8413)

Companion lemma to `eq_top_of_card_eq`.

Author: tb65536

src/group_theory/subgroup.lean

@@ -422,6 +422,9 @@ begin
   congr
 end
 
+@[to_additive] lemma eq_bot_of_card_eq [fintype H] (h : fintype.card H = 1) : H = ⊥ :=
+let _ := fintype.card_le_one_iff_subsingleton.mp (le_of_eq h) in by exactI eq_bot_of_subsingleton H
+
 @[to_additive] lemma nontrivial_iff_exists_ne_one (H : subgroup G) :
   nontrivial H ↔ ∃ x ∈ H, x ≠ (1:G) :=
 subtype.nontrivial_iff_exists_ne (λ x, x ∈ H) (1 : H)