map_geom_sum₂ — Mathlib

English

A ring homomorphism preserves sums of products x^i y^{n-1-i}: f(∑ x^i y^{n-1-i}) = ∑ f(x)^i f(y)^{n-1-i}.

Русский

Гомоморфизм кольца сохраняет суммы произведений x^i y^{n-1-i}: f(∑ x^i y^{n-1-i}) = ∑ f(x)^i f(y)^{n-1-i}.

LaTeX

$$$f\\left(\\sum_{i=0}^{n-1} x^{i} y^{n-1-i}\\right) = \\sum_{i=0}^{n-1} f(x)^{i} f(y)^{n-1-i}$$$

Lean4

theorem map_geom_sum₂ (x y : R) (n : ℕ) (f : R →+* S) :
    f (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ range n, f x ^ i * f y ^ (n - 1 - i) := by simp [map_sum f]

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