map — Mathlib

English

Under invertibility of 2, D_1 1 n equals (1/2) times Chebyshev T of n composed with 2X: D_1 1 n = (1/2) Chebyshev.T_R(n) ∘ (2X).

Русский

При обратимости 2 равенство D_1 1 n = (1/2) Chebyshev T_R(n) ∘ (2X).

LaTeX

$$dickson\, 1\, (1 : R)\, n = C (⅟2) * (Chebyshev.T\, R\, n).comp (2 * X)$$

Lean4

theorem map (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommSemiring A] (φ : R →+* A) :
    (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ) :=
  by
  refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
  rw [coeff_map]
  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))

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