toLinearMap_apply

Mathlib.Algebra.Algebra.Hom

URI: https://scilib.ai/kg/mathlib#AlgHom.toLinearMap_apply

English

For any φ: A →ₐ[R] B, and any p ∈ A, the associated linear map satisfies φ.toLinearMap(p) = φ(p).

Русский

Для любого гомоморфизма φ: A →ₐ[R] B и любого p ∈ A связанное линейное отображение удовлетворяет φ.toLinearMap(p) = φ(p).

LaTeX

$$$$\forall p\in A:\ \ φ.toLinearMap(p)=φ(p). $$$$

Lean4

@[simp]
theorem toLinearMap_apply (p : A) : φ.toLinearMap p = φ p :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru