monomial_def — Mathlib

English

The nth monomial is equal to the linear map single_R that sends the base to the coefficient at n.

Русский

nth моном — это линейное отображение single_R, которое отправляет базовый коэффициент на коэффициент при n.

LaTeX

$$$\\operatorname{monomial}(n) = \\operatorname{LinearMap.single} \\, R \\, (\\lambda _\\mapsto R) \\, n$$$

Lean4

theorem monomial_def [DecidableEq σ] (n : σ →₀ ℕ) : monomial n = LinearMap.single R (fun _ ↦ R) n :=
  by
  rw [monomial]
    -- unify the `Decidable` arguments

  convert rfl

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