coe_one

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

The embedding sends the identity to the identity.

Русский

Вложение отправляет тождественный элемент в тождественный элемент.

LaTeX

$$$\mathrm{coe}(1) = 1$$$

Lean4

theorem coe_one : coe 1 = 1 := by simp only [coe, map_one]

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

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

Разделы

Аффилиация

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