Theorems · Theorem · number theory

ModularGroup.tendsto_lcRow0

∀ {cd : Fin 2 → ℤ},
  IsCoprime (cd 0) (cd 1) →
    Filter.Tendsto (fun g => (ModularGroup.lcRow0 cd) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g))
      Filter.cofinite (Filter.cocompact ℝ)

The map lcRow0 is proper, that is, preimages of cocompact sets are finite in [[* , *], [c, d]].

Defined in

Mathlib.NumberTheory.Modular

Cited by

1 results in Mathlib

Foundations

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