xn_modEq_x4n_sub — Mathlib

English

For a > 1 and j ≤ 2n, xn(a1, 4n − j) ≡ xn(a1, j) (mod xn(a1, n)).

Русский

Пусть a > 1. При j ≤ 2n выполняется 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_sub {n j} (h : j ≤ 2 * n) : xn a1 (4 * n - j) ≡ xn a1 j [MOD xn a1 n] :=
  have h' : j ≤ 2 * n := le_trans h (by rw [Nat.succ_mul])
  ModEq.add_right_cancel' (xn a1 (2 * n - j)) <|
    by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']
    apply xn_modEq_x2n_add

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