id — Mathlib · SciLib

English

The identity hom on a generators family corresponds to the identity AlgHom on the polynomial ring.

Русский

Идентичный гомоморфизм генераторов соответствует идентичному AlgHom на кольце многочленов.

LaTeX

$$$\\text{Hom.id } P \\;:\\; \\text{Hom } P P \\to \\text{AlgHom } P.Ring P.Ring$ is the identity$$

Lean4

/-- The identity hom. -/
@[simps]
protected noncomputable def id : Hom P P :=
  ⟨X, by simp⟩

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