xn_modEq_x2n_sub — Mathlib

English

Let a > 1. If j ≤ 2n, then xn(a1, 2n − j) + xn(a1, j) ≡ 0 (mod xn(a1, n)).

Русский

Пусть a > 1. При j ≤ 2n верно xn(a1, 2n − j) + xn(a1, j) ≡ 0 (mod xn(a1, n)).

LaTeX

$$$$ xn(a1, 2n - j) + xn(a1, j) \\equiv 0 \\pmod{ xn(a1, n) } $$$$

Lean4

theorem xn_modEq_x2n_sub {n j} (h : j ≤ 2 * n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n] :=
  (le_total j n).elim (xn_modEq_x2n_sub_lem a1) fun jn =>
    by
    have : 2 * n - j + j ≤ n + j := by rw [tsub_add_cancel_of_le h, two_mul]; exact Nat.add_le_add_left jn _
    let t := xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
    rwa [tsub_tsub_cancel_of_le h, add_comm] at t

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