instFunLikeSubtypeMemSubsemiringCenter

English

The natural embedding of integers into CentroidHom α sends z ∈ ℤ to the endomorphism z • id_α.

Русский

Естественное вложение целых чисел в CentroidHom α отправляет z ∈ ℤ в эндоморфизм z • id_α.

LaTeX

$$$\text{coe_intCast}(z) = z \cdot \mathrm{id}_\alpha$$$

Lean4

instance : FunLike (Subsemiring.center (CentroidHom α)) α α
    where
  coe f := f.val.toFun
  coe_injective' f g
    h := by
    cases f
    cases g
    congr with x
    exact congrFun h x

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