id_comp

Mathlib.RingTheory.Extension.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.Hom.id_comp

English

Repeated: the trivial extension with Ring S and σ = id_S is the canonical example.

Русский

Повтор: тривиальное расширение с кольцом S и σ = id_S – канонический пример.

LaTeX

$$$\\text{self}$ is the Extension with Ring = S, σ = id_S, algebraMap_σ = rfl$$

Lean4

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

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

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

Разделы

Аффилиация

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