mod_left — Mathlib

English

For all a ∈ ℤ and b ∈ ℕ, J(a | b) = J(a mod b | b).

Русский

Пусть a ∈ ℤ и b ∈ ℕ. Тогда J(a | b) = J(a mod b | b).

LaTeX

$$$ J(a | b) = J(a \bmod b | b) $$$

Lean4

/-- The symbol `J(a | b)` depends only on `a` mod `b`. -/
theorem mod_left (a : ℤ) (b : ℕ) : J(a | b) = J(a % b | b) :=
  congr_arg List.prod <|
    List.pmap_congr_left _
      (by
        rintro p hp _ h₂
        conv_rhs =>
          rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <| dvd_of_mem_primeFactorsList hp), ←
            legendreSym.mod])

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