coe_one

Mathlib.Topology.Algebra.ContinuousMonoidHom

URI: https://scilib.ai/kg/mathlib#ContinuousMonoidHom.coe_one

English

The unique map sending every element to the multiplicative identity is preserved under the appropriate coe and equals the usual identity map when interpreted appropriately.

Русский

Единичная карта сохраняется при приводке и соответствует обычной единице.

LaTeX

$$$coe\\_one: (A\\to_* B)\\to_* 1$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_one : ⇑(1 : A →ₜ* B) = 1 :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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