coeHom_apply

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

The canonical homogeneous embedding agrees with the direct inclusion: coeHom(g) = coe(g).

Русский

Каноническое вложение согласуется с прямым включением: coeHom(g) = coe(g).

LaTeX

$$$\mathrm{coeHom}(g) = \mathrm{coe}(g)$$$

Lean4

@[simp]
theorem coeHom_apply (g : SL(2, ℤ)) : coeHom g = coe g :=
  rfl

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

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

Разделы

Аффилиация

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