xn_modEq_x4n_add — Mathlib

English

For a > 1, and integers n, j, we have xn(a1, 4n + j) ≡ xn(a1, j) (mod xn(a1, n)).

Русский

Для a > 1 выполняется xn(a1, 4n + j) ≡ xn(a1, j) (mod xn(a1, n)).

LaTeX

$$$$ xn(a1, 4n + j) \\equiv xn(a1, j) \\pmod{ xn(a1, n) } $$$$

Lean4

theorem xn_modEq_x4n_add (n j) : xn a1 (4 * n + j) ≡ xn a1 j [MOD xn a1 n] :=
  ModEq.add_right_cancel' (xn a1 (2 * n + j)) <|
    by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]
    apply xn_modEq_x2n_add

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