at_neg_one — Mathlib

English

For odd b, J(-1 | b) is given by χ₄(b).

Русский

Для нечётного b, J(-1 | b) задаётся χ₄(b).

LaTeX

$$$ J(-1 | b) = χ_4(b) $$$

Lean4

/-- If `b` is odd, then `J(-1 | b)` is given by `χ₄ b`. -/
theorem at_neg_one {b : ℕ} (hb : Odd b) : J(-1 | b) = χ₄ b :=
  -- Porting note: In mathlib3, it was written `χ₄` and Lean could guess that it had to use
    -- `χ₄.to_monoid_hom`. This is not the case with Lean 4.

  value_at (-1) χ₄.toMonoidHom (fun p pp => @legendreSym.at_neg_one p ⟨pp⟩) hb

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