instRing — Mathlib

English

If M is an AddCommGroup, then AddMonoid.End(M) is a ring (with the natural semiring structure extended by additive inverses).

Русский

Если M — AddCommGroup, то End(M) образует кольцо (с естественной полукольцевой структурой и дополнением).

LaTeX

$$End(M) is a Ring when M is AddCommGroup.$$

Lean4

instance instRing [AddCommGroup M] : Ring (AddMonoid.End M) :=
  { AddMonoid.End.instSemiring, AddMonoid.End.instAddCommGroup with intCast := fun z => z • (1 : AddMonoid.End M),
    intCast_ofNat := natCast_zsmul _, intCast_negSucc := negSucc_zsmul _ }

Похожие утверждения