Pointwise instances on Subgroup and AddSubgroups #
This file provides the actions
which matches the action of Set.mulActionSet.
These actions are available in the Pointwise locale.
Implementation notes #
The pointwise section of this file is almost identical to
the file Mathlib.Algebra.Group.Submonoid.Pointwise.
Where possible, try to keep them in sync.
@[simp]
theorem
inv_coe_set
{G : Type u_2}
{S : Type u_4}
[InvolutiveInv G]
[SetLike S G]
[InvMemClass S G]
{H : S}
:
@[simp]
theorem
neg_coe_set
{G : Type u_2}
{S : Type u_4}
[InvolutiveNeg G]
[SetLike S G]
[NegMemClass S G]
{H : S}
:
@[simp]
theorem
smul_coe_set
{G : Type u_2}
{S : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
@[simp]
theorem
vadd_coe_set
{G : Type u_2}
{S : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
@[simp]
theorem
op_smul_coe_set
{G : Type u_2}
{S : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
MulOpposite.op a • ↑s = ↑s
@[simp]
theorem
op_vadd_coe_set
{G : Type u_2}
{S : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
AddOpposite.op a +ᵥ ↑s = ↑s
@[simp]
theorem
coe_div_coe
{G : Type u_2}
{S : Type u_4}
[SetLike S G]
[DivisionMonoid G]
[SubgroupClass S G]
(H : S)
:
@[simp]
theorem
coe_sub_coe
{G : Type u_2}
{S : Type u_4}
[SetLike S G]
[SubtractionMonoid G]
[AddSubgroupClass S G]
(H : S)
:
@[simp]
theorem
Set.mul_subgroupClosure
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
:
s * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
@[simp]
theorem
Set.add_addSubgroupClosure
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
:
s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.subgroupClosure_mul
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
:
↑(Subgroup.closure s) * s = ↑(Subgroup.closure s)
@[simp]
theorem
Set.addSubgroupClosure_add
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
:
↑(AddSubgroup.closure s) + s = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.pow_mul_subgroupClosure
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
s ^ n * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
@[simp]
theorem
Set.nsmul_add_addSubgroupClosure
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
n • s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.subgroupClosure_mul_pow
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
↑(Subgroup.closure s) * s ^ n = ↑(Subgroup.closure s)
@[simp]
theorem
Set.addSubgroupClosure_add_nsmul
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
↑(AddSubgroup.closure s) + n • s = ↑(AddSubgroup.closure s)
@[simp]
theorem
Subgroup.inv_subset_closure
{G : Type u_2}
[Group G]
(S : Set G)
:
S⁻¹ ⊆ ↑(Subgroup.closure S)
@[simp]
theorem
AddSubgroup.neg_subset_closure
{G : Type u_2}
[AddGroup G]
(S : Set G)
:
-S ⊆ ↑(AddSubgroup.closure S)
theorem
Subgroup.closure_toSubmonoid
{G : Type u_2}
[Group G]
(S : Set G)
:
(Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
theorem
AddSubgroup.closure_toAddSubmonoid
{G : Type u_2}
[AddGroup G]
(S : Set G)
:
(AddSubgroup.closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)
theorem
Subgroup.closure_induction_left
{G : Type u_2}
[Group G]
{s : Set G}
{p : (x : G) → x ∈ Subgroup.closure s → Prop}
(one : p 1 ⋯)
(mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯)
(inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
For subgroups generated by a single element, see the simpler zpow_induction_left.
theorem
AddSubgroup.closure_induction_left
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (x : G) → x ∈ AddSubgroup.closure s → Prop}
(one : p 0 ⋯)
(mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯)
(inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
For additive subgroups generated by a single element, see the simpler
zsmul_induction_left.
theorem
Subgroup.closure_induction_right
{G : Type u_2}
[Group G]
{s : Set G}
{p : (x : G) → x ∈ Subgroup.closure s → Prop}
(one : p 1 ⋯)
(mul_right : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯)
(mul_inv_cancel : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
For subgroups generated by a single element, see the simpler zpow_induction_right.
theorem
AddSubgroup.closure_induction_right
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (x : G) → x ∈ AddSubgroup.closure s → Prop}
(one : p 0 ⋯)
(mul_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯)
(mul_inv_cancel : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
For additive subgroups generated by a single element, see the simpler
zsmul_induction_right.
@[simp]
@[simp]
@[simp]
theorem
Subgroup.closure_singleton_inv
{G : Type u_2}
[Group G]
(x : G)
:
Subgroup.closure {x⁻¹} = Subgroup.closure {x}
@[simp]
theorem
AddSubgroup.closure_singleton_neg
{G : Type u_2}
[AddGroup G]
(x : G)
:
AddSubgroup.closure {-x} = AddSubgroup.closure {x}
theorem
Subgroup.closure_induction''
{G : Type u_2}
[Group G]
{s : Set G}
{p : (g : G) → g ∈ Subgroup.closure s → Prop}
(mem : ∀ (x : G) (hx : x ∈ s), p x ⋯)
(inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯)
(one : p 1 ⋯)
(mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
An induction principle for closure membership. If p holds for 1 and all elements of
k and their inverse, and is preserved under multiplication, then p holds for all elements of
the closure of k.
theorem
AddSubgroup.closure_induction''
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (g : G) → g ∈ AddSubgroup.closure s → Prop}
(mem : ∀ (x : G) (hx : x ∈ s), p x ⋯)
(inv_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯)
(one : p 0 ⋯)
(mul : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
An induction principle for additive closure membership. If p holds for 0 and all
elements of k and their negation, and is preserved under addition, then p holds for all
elements of the additive closure of k.
theorem
Subgroup.iSup_induction
{G : Type u_2}
[Group G]
{ι : Sort u_5}
(S : ι → Subgroup G)
{C : G → Prop}
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
(mem : ∀ (i : ι), ∀ x ∈ S i, C x)
(one : C 1)
(mul : ∀ (x y : G), C x → C y → C (x * y))
:
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 1 and all elements of S i for all i, and is preserved under multiplication,
then it holds for all elements of the supremum of S.
theorem
AddSubgroup.iSup_induction
{G : Type u_2}
[AddGroup G]
{ι : Sort u_5}
(S : ι → AddSubgroup G)
{C : G → Prop}
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
(mem : ∀ (i : ι), ∀ x ∈ S i, C x)
(one : C 0)
(mul : ∀ (x y : G), C x → C y → C (x + y))
:
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 0 and all elements of S i for all i, and is preserved under addition,
then it holds for all elements of the supremum of S.
theorem
Subgroup.iSup_induction'
{G : Type u_2}
[Group G]
{ι : Sort u_5}
(S : ι → Subgroup G)
{C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop}
(hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯)
(h1 : C 1 ⋯)
(hmul : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x * y) ⋯)
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
:
C x hx
A dependent version of Subgroup.iSup_induction.
theorem
AddSubgroup.iSup_induction'
{G : Type u_2}
[AddGroup G]
{ι : Sort u_5}
(S : ι → AddSubgroup G)
{C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop}
(hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯)
(h1 : C 0 ⋯)
(hmul : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x + y) ⋯)
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
:
C x hx
A dependent version of AddSubgroup.iSup_induction.
theorem
Subgroup.closure_mul_le
{G : Type u_2}
[Group G]
(S T : Set G)
:
Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T
theorem
AddSubgroup.closure_add_le
{G : Type u_2}
[AddGroup G]
(S T : Set G)
:
AddSubgroup.closure (S + T) ≤ AddSubgroup.closure S ⊔ AddSubgroup.closure T
theorem
Subgroup.closure_pow_le
{G : Type u_2}
[Group G]
{s : Set G}
{n : ℕ}
:
n ≠ 0 → Subgroup.closure (s ^ n) ≤ Subgroup.closure s
theorem
AddSubgroup.closure_nsmul_le
{G : Type u_2}
[AddGroup G]
{s : Set G}
{n : ℕ}
:
n ≠ 0 → AddSubgroup.closure (n • s) ≤ AddSubgroup.closure s
theorem
Subgroup.closure_pow
{G : Type u_2}
[Group G]
{s : Set G}
{n : ℕ}
(hs : 1 ∈ s)
(hn : n ≠ 0)
:
Subgroup.closure (s ^ n) = Subgroup.closure s
theorem
AddSubgroup.closure_nsmul
{G : Type u_2}
[AddGroup G]
{s : Set G}
{n : ℕ}
(hs : 0 ∈ s)
(hn : n ≠ 0)
:
AddSubgroup.closure (n • s) = AddSubgroup.closure s
theorem
Subgroup.sup_eq_closure_mul
{G : Type u_2}
[Group G]
(H K : Subgroup G)
:
H ⊔ K = Subgroup.closure (↑H * ↑K)
theorem
AddSubgroup.sup_eq_closure_add
{G : Type u_2}
[AddGroup G]
(H K : AddSubgroup G)
:
H ⊔ K = AddSubgroup.closure (↑H + ↑K)
theorem
AddSubgroup.set_add_normal_comm
{G : Type u_2}
[AddGroup G]
(s : Set G)
(N : AddSubgroup G)
[hN : N.Normal]
:
The carrier of H ⊔ N is just ↑H + ↑N (pointwise set addition)
when N is normal.
The carrier of N ⊔ H is just ↑N + ↑H (pointwise set addition)
when N is normal.
instance
AddSubgroup.sup_normal
{G : Type u_2}
[AddGroup G]
(H K : AddSubgroup G)
[hH : H.Normal]
[hK : K.Normal]
:
(H ⊔ K).Normal
Pointwise action #
def
Subgroup.pointwiseMulAction
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
:
The action on a subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise locale.
Equations
Instances For
theorem
Subgroup.pointwise_smul_def
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
{a : α}
(S : Subgroup G)
:
a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S
instance
Subgroup.instCovariantClassHSMulLe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
:
theorem
Subgroup.smul_closure
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
(a : α)
(s : Set G)
:
a • Subgroup.closure s = Subgroup.closure (a • s)
instance
Subgroup.pointwise_isCentralScalar
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
[MulDistribMulAction αᵐᵒᵖ G]
[IsCentralScalar α G]
:
IsCentralScalar α (Subgroup G)
def
Subgroup.equivSMul
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
:
Applying a MulDistribMulAction results in an isomorphic subgroup
Equations
- Subgroup.equivSMul a H = (MulDistribMulAction.toMulEquiv G a).subgroupMap H
Instances For
@[simp]
theorem
Subgroup.equivSMul_apply_coe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
(x : ↑↑H.toSubmonoid)
:
↑((Subgroup.equivSMul a H) x) = a • ↑x
@[simp]
theorem
Subgroup.equivSMul_symm_apply_coe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
(y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid))
:
↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y
@[simp]
theorem
Subgroup.smul_mem_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
theorem
Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
theorem
Subgroup.mem_inv_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
@[simp]
theorem
Subgroup.pointwise_smul_le_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
theorem
Subgroup.pointwise_smul_le_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
theorem
Subgroup.le_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
def
AddSubgroup.pointwiseMulAction
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
:
MulAction α (AddSubgroup A)
The action on an additive subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise locale.
Equations
Instances For
theorem
AddSubgroup.pointwise_smul_def
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
{a : α}
(S : AddSubgroup A)
:
a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd α A) a) S
@[simp]
theorem
AddSubgroup.coe_pointwise_smul
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(a : α)
(S : AddSubgroup A)
:
@[simp]
theorem
AddSubgroup.pointwise_smul_toAddSubmonoid
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(a : α)
(S : AddSubgroup A)
:
theorem
AddSubgroup.smul_mem_pointwise_smul
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(m : A)
(a : α)
(S : AddSubgroup A)
:
theorem
AddSubgroup.mem_smul_pointwise_iff_exists
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(m : A)
(a : α)
(S : AddSubgroup A)
:
instance
AddSubgroup.pointwise_isCentralScalar
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
[DistribMulAction αᵐᵒᵖ A]
[IsCentralScalar α A]
:
IsCentralScalar α (AddSubgroup A)
@[simp]
theorem
AddSubgroup.smul_mem_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
theorem
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
theorem
AddSubgroup.mem_inv_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
@[simp]
theorem
AddSubgroup.pointwise_smul_le_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
theorem
AddSubgroup.pointwise_smul_le_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
theorem
AddSubgroup.le_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
@[simp]
theorem
AddSubgroup.smul_mem_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
theorem
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
theorem
AddSubgroup.mem_inv_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
@[simp]
theorem
AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
theorem
AddSubgroup.pointwise_smul_le_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
theorem
AddSubgroup.le_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
@[simp]
theorem
AddSubgroup.zero_smul
{R : Type u_5}
{M : Type u_6}
[Semiring R]
[AddCommGroup M]
[Module R M]
(s : AddSubgroup M)
:
For additive subgroups S and T of a ring, the product of S and T as submonoids
is automatically a subgroup, which we define as the product of S and T as subgroups.
Equations
- AddSubgroup.mul = { mul := fun (M N : AddSubgroup R) => let __spread.0 := M.toAddSubmonoid * N.toAddSubmonoid; { toAddSubmonoid := __spread.0, neg_mem' := ⋯ } }
Instances For
theorem
AddSubgroup.mul_toAddSubmonoid
{R : Type u_5}
[NonUnitalNonAssocRing R]
(M N : AddSubgroup R)
: