Additive subgroups of rings

@[instance_reducible]

def AddSubgroup.mul {R : Type u_1} [NonUnitalNonAssocRing R] : Mul (AddSubgroup R)

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' := ⋯ } }

theorem AddSubgroup.mul_toAddSubmonoid {R : Type u_1} [NonUnitalNonAssocRing R] (M N : AddSubgroup R) : (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid

@[simp]

theorem AddSubgroup.zero_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] (s : AddSubgroup M) : 0 • s = ⊥