coe

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.Simps.coe

English

The Simps.coe projection is the identity on the underlying ContinuousAlgHom when viewed as a map A →ₐ[R] B.

Русский

Проекция Simps.coe является тождественной при рассмотрении как отображение A →ₐ[R] B.

LaTeX

$$$\\text{ContinuousAlgHom.Simps.coe}\\; h : A \\to A[R] B : A \\to B$$$

Lean4

/-- See Note [custom simps projection]. -/
def coe (h : A →A[R] B) : A →ₐ[R] B :=
  h

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

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

Разделы

Аффилиация

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