coe_mk'

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.coe_mk'

English

The projection from a constructed ContinuousAlgHom to its underlying AlgHom is the identity on the constructed object.

Русский

Проекция из построенного ContinuousAlgHom к базовому AlgHom является тождественной на построенном объекте.

LaTeX

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

Lean4

@[simp]
theorem coe_mk' (f : A →ₐ[R] B) (h) : (mk f h : A → B) = f :=
  rfl

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

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

Разделы

Аффилиация

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