Nyll.AlgebraicCurves.Foundations.Algebra.Subgroup_IsArithmetic_exists_nat_mem_strictPeriods_conj

theorem

exists_nat_mem_strictPeriods_conj

Subgroup.IsArithmetic.exists_nat_mem_strictPeriods_conj

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Subgroup_IsArithmetic_exists_nat_mem_strictPeriods_conj
open Matrix.SpecialLinearGroup ConjAct
open scoped MatrixGroups Pointwise
noncomputable section

Lean source · statement

theorem _root_.Subgroup.IsArithmetic.exists_nat_mem_strictPeriods_conj (𝒢 : Subgroup (GL (Fin 2)
  ℝ)) [𝒢.IsArithmetic] : ∃ M : ℕ, 0 < M ∧ ∀ γ : SL(2, ℤ), (M : ℝ) ∈ (ConjAct.toConjAct
  (Matrix.SpecialLinearGroup.mapGL ℝ γ) • 𝒢).strictPeriods

Subgroup_IsArithmetic_exists_nat_mem_strictPeriods_conj.lean

Module documentation

Subgroup Is Arithmetic exists nat mem strict Periods conj

exists_nat_mem_strictPeriods_conj

Module documentation

Subgroup Is Arithmetic exists nat mem strict Periods conj

Declarations

exists_nat_mem_strictPeriods_conj