commutes — Mathlib

English

Algebra equivalences preserve the algebra structure, and the action commutes with algebra maps; i.e., the map from R into A2 via algebraMap commutes with e.

Русский

Алгебраические эквивалентности сохраняют структуру алгебры и совместимы с отображениями алгебраического отображения; т.е. диаграммы коммутируют.

LaTeX

$$$ e(r) = r \text{ in } A_2 \text{ for all } r \in R $ and the diagram commutes.$$

Lean4

@[simp]
theorem commutes : ∀ r : R, e (algebraMap R A₁ r) = algebraMap R A₂ r :=
  e.commutes'

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