Theorems · Theorem · number theory

OnePoint.exists_mem_SL2

∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (A : Type u_2) [inst_2 : CommRing A] [IsDomain A]
  [inst_4 : Algebra A K] [IsFractionRing A K] [IsPrincipalIdealRing A] (c : OnePoint K),
  ∃ g, (Matrix.SpecialLinearGroup.mapGL K) g • OnePoint.infty = c

The modular group SL(2, A) acts transitively on OnePoint K, if A is a PID whose fraction field is K. (This includes the case A = ℤ, K = ℚ.)

Defined in

Mathlib.NumberTheory.ModularForms.Cusps

Cited by

2 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEqCommRingIsDomainAlgebraIsFractionRingIsPrincipalIdealRing