map — Mathlib

English

The Bernstein polynomial with base ring R maps under any ring hom f to the Bernstein polynomial over S with the same indices.

Русский

Полином Бернштейна над кольцом R отображается гомоморфизмом f в полином Бернштейна над кольцом S с теми же индексами.

LaTeX

$$$\forall f:\, R \to+* S,\; (\bernsteinPolynomial R n \nu).map f = \bernsteinPolynomial S n \nu$$$

Lean4

@[simp]
theorem map (f : R →+* S) (n ν : ℕ) : (bernsteinPolynomial R n ν).map f = bernsteinPolynomial S n ν := by
  simp [bernsteinPolynomial]

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