const_algebraMap — Mathlib

English

For every k ∈ K, the constant simple function with value algebraMap K β k is exactly the algebraMap K (α →ₛ β) applied to k.

Русский

Для каждого элемента k ∈ K константная простая функция со значением algebraMap K β k равна алгебраическому отображению algebraMap K (α →ₛ β) от k.

LaTeX

$$$\\const_{\\alpha}(\\text{algebraMap}_{K}^{\\beta} (k)) = \\text{algebraMap}_{K}^{\\alpha \\to_{\\mathcal{S}} \\beta}(k).$$$

Lean4

@[simp]
theorem const_algebraMap [CommSemiring K] [Semiring β] [Algebra K β] (k : K) :
    const α (algebraMap K β k) = algebraMap K (α →ₛ β) k :=
  rfl

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