Documentation

PFR.Mathlib.Algebra.Group.Subgroup.Pointwise

source
@[simp]
theorem AddSubgroupClass.coe_add_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [SubNegMonoid G] [AddSubgroupClass S G] (H : S) :
↑H + ↑H = ↑H
source
@[simp]
theorem SubgroupClass.coe_mul_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [DivInvMonoid G] [SubgroupClass S G] (H : S) :
↑H * ↑H = ↑H
source
@[simp]
theorem AddSubgroupClass.neg_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [SubtractionMonoid G] [AddSubgroupClass S G] (H : S) :
-↑H = ↑H
source
@[simp]
theorem SubgroupClass.inv_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) :
(↑H)⁻¹ = ↑H
source
@[simp]
theorem AddSubgroupClass.coe_sub_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [SubtractionMonoid G] [AddSubgroupClass S G] (H : S) :
↑H - ↑H = ↑H
source
@[simp]
theorem SubgroupClass.coe_div_coe {S : Type u_1} {G : Type u_2} [SetLike S G] [DivisionMonoid G] [SubgroupClass S G] (H : S) :
↑H / ↑H = ↑H