Documentation

Mathlib.Algebra.Ring.Subgroup

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
Instances For
    @[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 =