coe_mk'

Mathlib.Algebra.Star.StarAlgHom

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

English

A variant of coe_mk for a plain AlgHom with star compatibility yields the same underlying map.

Русский

Вариант coe_mk для простого AlgHom с сохранением звезды ведёт к той же базовой карте.

LaTeX

$$$((⟨f, h⟩ : A \to⋆ₐ[R] B) : A \to B) = f$$$

Lean4

@[simp]
theorem coe_mk' (f : A →ₐ[R] B) (h) : ((⟨f, h⟩ : A →⋆ₐ[R] B) : A → B) = f :=
  rfl

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

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

Разделы

Аффилиация

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