Theorems · Theorem · number theory

EisensteinSeries.vecMulSL_gcd

∀ {r : ℕ} [NeZero r] {v : Fin 2 → ℤ},
  EisensteinSeries.finGcdMap v = r →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), EisensteinSeries.finGcdMap (Matrix.vecMul v ↑A) = r

Right-multiplying a vector by a matrix in SL(2, ℤ) doesn't change its gcd.

Defined in: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Matrixstatement · cited by 4,303
mul_oneproof · cited by 3,885
Matrix.detstatement · cited by 665
Int.cast_natCastproof · cited by 393
nsmul_eq_mulproof · cited by 369
Matrix.SpecialLinearGroupstatement and proof · cited by 348
Fintype.elemsproof · cited by 194
Fintype.completeproof · cited by 192
Matrix.vecMulstatement and proof · cited by 148
zsmul_eq_mulproof · cited by 120
Int.isCoprime_iff_gcd_eq_oneproof · cited by 16
EisensteinSeries.finGcdMapstatement and proof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

EisensteinSeries.vecMul_SL2_mem_gammaSetproof · cited by 0