algebraMap_monomial — Mathlib

English

For any n ∈ ℕ and a ∈ K, the image of the monomial monomial n a under the embedding is C(a) X^n.

Русский

Для любого натурального n и элемента a ∈ K образ мономиала monomial n a через вложение равен C(a) X^n.

LaTeX

$$$ \mathrm{algebraMap}_{K[X] \to \mathrm{RatFunc} K}(\mathrm{Polynomial.monomial} n a) = \mathrm{C}(a) \cdot \mathrm{X}^n $$$

Lean4

@[simp]
theorem algebraMap_monomial (n : ℕ) (a : K) : algebraMap K[X] (RatFunc K) (Polynomial.monomial n a) = C a * X ^ n := by
  simp [← Polynomial.C_mul_X_pow_eq_monomial]

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