instHasDetPlusMinusOneOfHasDetOne

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

URI: https://scilib.ai/kg/mathlib#Subgroup.instHasDetPlusMinusOneOfHasDetOne

English

IsArithmetic Γ ↔ FiniteIndex Γ (for appropriate Γ).

Русский

Для подходящей подгруппы Γ равносильно: Γ арифметическая тогда и только тогда, когда имеет конечный индекс.

LaTeX

$$$IsArithmetic(\Gamma) \Leftrightarrow Γ.FiniteIndex$$$

Lean4

instance [HasDetOne Γ] : HasDetPlusMinusOne Γ :=
  ⟨fun {g} hg ↦ by simp [HasDetOne.det_eq hg]⟩

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

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

Разделы

Аффилиация

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