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

Companion lemma to `eq_top_of_card_eq`.
leanprover-community · Jul 24, 2021 · 02b37b5 · 02b37b5
1 parent 8a0d5e0
commit 02b37b5
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/group_theory/subgroup.lean b/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)