feat: a subgroup is 1 iff it's trivial (#17906)

From LeanCamCombi
leanprover-community · Oct 18, 2024 · 344c0bb · 344c0bb
1 parent e84469b
commit 344c0bb
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@@ -41,6 +41,10 @@ lemma smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (
     a • (s : Set G) = s := by
   ext; simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left, ha]
 
+@[norm_cast, to_additive]
+lemma coe_set_eq_one [Group G] {s : Subgroup G} : (s : Set G) = 1 ↔ s = ⊥ :=
+  (SetLike.ext'_iff.trans (by rfl)).symm
+
 @[to_additive (attr := simp)]
 lemma op_smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
     MulOpposite.op a • (s : Set G) = s := by