id

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#AlgHom.id

English

The coe of mk' f h to a RingHom equals f exactly.

Русский

Сопоставление mk' f h как RingHom равно f.

LaTeX

$$$\\text{coe\\_mk'}(f,h) : (mk' f h) = f$$$

Lean4

/-- Identity map as an `AlgHom`. -/
protected def id : A →ₐ[R] A :=
  { RingHom.id A with commutes' := fun _ => rfl }

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

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

Разделы

Аффилиация

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