toEndRingHom — Mathlib

English

CentroidHom α forms a semiring by transporting the semiring structure of End α along the natural embedding.

Русский

CentroidHom α образует полукольцо, полученное переносом структуры полукольца End α через естественное вложение.

LaTeX

$$$Semiring(\mathrm{CentroidHom}(\alpha))$$$

Lean4

/-- `CentroidHom.toEnd` as a `RingHom`. -/
@[simps]
def toEndRingHom : CentroidHom α →+* AddMonoid.End α
    where
  toFun := toEnd
  map_zero' := toEnd_zero
  map_one' := toEnd_one
  map_add' := toEnd_add
  map_mul' := toEnd_mul

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