toAlgHom_id

Mathlib.RingTheory.Extension.Generators

URI: https://scilib.ai/kg/mathlib#Algebra.Generators.Hom.toAlgHom_id

English

Composition with the identity generator hom leaves the second hom unchanged: f.comp id = f.

Русский

Слоение с идентичным гомоморфизмом генераторов не меняет гомоморфизм: f.comp id = f.

LaTeX

$$$f.\\mathrm{comp}(\\mathrm{id}) = f$$$

Lean4

@[simp]
theorem toAlgHom_id : Hom.toAlgHom (.id P) = AlgHom.id _ _ := by ext1; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru