toCentroidHom — Mathlib

English

The scalar tower axioms hold for the action of CentroidHom α on α with α’s action, i.e., smul_assoc for CentroidHom α and α on α.

Русский

Секторальные аксиомы для действия CentroidHom α на α совместимы с действием α на α, i.e., соблюдается smul_assoc.

LaTeX

$$$\text{IsScalarTower } (\mathrm{CentroidHom}(\alpha)) \; \alpha \; \alpha$$$

Lean4

/-- The natural ring homomorphism from `R` into `CentroidHom α`.

This is a stronger version of `Module.toAddMonoidEnd`. -/
@[simps! apply_toFun]
def _root_.Module.toCentroidHom : R →+* CentroidHom α :=
  RingHom.smulOneHom

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