reciprocalFactors_even — Mathlib

English

If n is a nonzero even number, then the sequence reciprocalFactors(n) begins with 3 followed by reciprocalFactors(n/2).

Русский

Пусть n — ненулевое чётное число. Тогда последовательность reciprocalFactors(n) начинается с 3 и продолжается как reciprocalFactors(n/2).

LaTeX

$$$ \operatorname{reciprocalFactors}(n) = 3 \,::\, \operatorname{reciprocalFactors}(n/2), \quad n \neq 0 \land \operatorname{Even}(n). $$$

Lean4

theorem reciprocalFactors_even {n : ℕ} (h0 : n ≠ 0) (h2 : Even n) :
    reciprocalFactors n = 3 :: reciprocalFactors (n / 2) :=
  by
  have h1 : n ≠ 1 := by
    rintro rfl
    norm_num at h2
  rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_pos h2]

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