starRingOfCommCentroidHom — Mathlib

English

If α has a commutative centroid, then the centroid carries a star-ring structure.

Русский

Если центр α коммутативен, то центроид обладает звездным кольцом.

LaTeX

$$$\\text{If } \\text{Std.Commutative}(\\alpha, \\mathrm{CentroidHom}(\\alpha)) \\text{ then } \\mathrm{CentroidHom}(\\alpha) \\text{ is a StarRing}$$$

Lean4

/-- Let `α` be a star ring with commutative centroid. Then the centroid is a star ring.
-/
@[reducible]
def starRingOfCommCentroidHom (mul_comm : Std.Commutative (α := CentroidHom α) (· * ·)) : StarRing (CentroidHom α)
    where
  __ := instStarAddMonoid
  star_mul _
    _ := ext (fun _ => by rw [mul_comm.comm, star_apply, mul_apply, mul_apply, star_apply, star_apply, star_star])

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