commutes

Mathlib.Algebra.Algebra.Hom

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

English

An R-algebra hom φ preserves scalar multiplication, i.e., φ(a) for a = algebraMap_R A r equals algebraMap_R B r.

Русский

Алгомоморфизм φ сохраняет скалярное умножение: φ(algebraMap_R A r) = algebraMap_R B r.

LaTeX

$$$\\forall r \\in R,\\; φ(\\text{algebraMap}_R A r) = \\text{algebraMap}_R B r$$$

Lean4

@[simp]
theorem commutes (r : R) : φ (algebraMap R A r) = algebraMap R B r :=
  φ.commutes' r

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

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

Разделы

Аффилиация

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