Documentation

Mathlib.Algebra.Ring.Subgroup

Additive subgroups of rings #

source
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
    Instances For
      source
      theorem AddSubgroup.mul_toAddSubmonoid {R : Type u_1} [NonUnitalNonAssocRing R] (M N : AddSubgroup R) :
      (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
      source
      @[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 = ⊥