From 344c0bb0e582a25235a93bb531130cb0433c6392 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 18 Oct 2024 14:18:26 +0000 Subject: [PATCH] feat: a subgroup is `1` iff it's trivial (#17906) From LeanCamCombi --- Mathlib/Algebra/Group/Subgroup/Pointwise.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean index 95c62df222f42..f42601fa4cc09 100644 --- 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