reciprocalFactors_odd — Mathlib

English

If n is odd and n ≠ 1, then reciprocalFactors(n) = (n mod 4) · n :: reciprocalFactors(n/4 + 1).

Русский

Пусть n нечётно и не равно 1. Тогда reciprocalFactors(n) = (n mod 4) · n :: reciprocalFactors(n/4 + 1).

LaTeX

$$$ \operatorname{reciprocalFactors}(n) = (n \bmod 4) \cdot n \,::\, \operatorname{reciprocalFactors}(n/4 + 1), \quad n \neq 1 \land \operatorname{Odd}(n). $$$

Lean4

theorem reciprocalFactors_odd {n : ℕ} (h1 : n ≠ 1) (h2 : Odd n) :
    reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1) :=
  by
  have h0 : n ≠ 0 := by
    rintro rfl
    norm_num [← Nat.not_even_iff_odd] at h2
  rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]

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