id_comp — Mathlib

English

Equality of Hom extends to equality of the corresponding toAlgHom constructions, via aeval congruence.

Русский

Равенство Hom тождественно распространяется на равенство соответствующих toAlgHom через соглaсование aeval.

LaTeX

$$$f=f' \\Rightarrow toAlgHom(f) = toAlgHom(f')$$$

Lean4

@[simp]
theorem id_comp [Algebra S S'] (f : Hom P P') : (Hom.id P').comp f = f := by ext; simp [Hom.id, aeval_X_left]

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