Additive subgroups of rings #
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_1}
[NonUnitalNonAssocRing R]
(M N : AddSubgroup R)
:
@[simp]
theorem
AddSubgroup.zero_smul
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommGroup M]
[Module R M]
(s : AddSubgroup M)
: