ofScalars_apply_eq — Mathlib

English

For x ∈ E and n ∈ ℕ, the nth coefficient evaluated at the constant element x is given by c(n) times x^n in a natural sense: ofScalars E c n (constant x) = c(n) · x^n.

Русский

Для x ∈ E и n ∈ ℕ, n-й коэффициент, взятый на константный элемент x, равен c(n)·x^n.

LaTeX

$$$\forall x\in E,\ \forall n\in\mathbb{N},\ (\operatorname{ofScalars} E c n)(\text{const } x) = c(n) \cdot x^{n}$$$

Lean4

theorem ofScalars_apply_eq (x : E) (n : ℕ) : ofScalars E c n (fun _ ↦ x) = c n • x ^ n := by simp [ofScalars]

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