linearMap — Mathlib

English

The linear map corresponding to Algebra.linearMap coincides with algebraMap as a function.

Русский

Линейное отображение, связанное с Algebra.linearMap, совпадает по функции с algebraMap.

LaTeX

$$$\mathrm{Algebra.linearMap}(R,A) = \mathrm{algebraMap}(R,A)$$$

Lean4

/-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,
packaged as an `R`-linear map.
-/
protected def linearMap : R →ₗ[R] A :=
  { algebraMap R A with map_smul' := fun x y => by simp [Algebra.smul_def] }

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