algebraMap_star_comm — Mathlib

English

For any r in R, the star of its image under the algebra map equals the image of the star: algebraMap(r)^* = algebraMap(r^*).

Русский

Для любого r ∈ R звезда изображения через алгебраическую карту равна изображению звезды: algebraMap(r)^* = algebraMap(r^*).

LaTeX

$$$\text{algebraMap } R A (\star r) = \star (\text{algebraMap } R A r)$$$

Lean4

@[simp]
theorem algebraMap_star_comm (r : R) : algebraMap R A (star r) = star (algebraMap R A r) := by
  simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]

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