det_coe

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

← MathLib Explorer

English

The determinant is preserved under the embedding: det(coe(g)) = 1 for all g ∈ SL(2, ℤ).

Русский

Определитель сохраняется под вложением: det(coe(g)) = 1 для всех g ∈ SL(2, ℤ).

LaTeX

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

Lean4

@[simp]
theorem det_coe {g : SL(2, ℤ)} : det (Units.val <| Subtype.val <| coe g) = 1 := by
  simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe]

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

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

Разделы

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

Аффилиация

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