S_eq_U_comp_half_mul_X — Mathlib

English

Assume 2 is invertible in R. Then for every integer n, S_R(n) = (U_R(n)).comp( (1/2) · X ).

Русский

Пусть 2 обратимо в R. Тогда для каждого n верно S_R(n) = (U_R(n)).comp((1/2)·X).

LaTeX

$$$ S_R(n) = (U_R(n)).\circ(\frac{1}{2} X) $$$

Lean4

theorem S_eq_U_comp_half_mul_X [Invertible (2 : R)] (n : ℤ) : S R n = (U R n).comp (Polynomial.C ⅟2 * X) :=
  by
  have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (S_comp_two_mul_X R n)
  simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul, Nat.cast_ofNat,
    mul_invOf_self', map_one, one_mul, comp_X] at this
  assumption

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