of_algebraMap_eq — Mathlib

English

There exists a StarAlgEquiv between Unitization R s and StarAlgebra.adjoin generated by s.

Русский

Существует звездно-алгебраическое эквивалентство между единичизацией и адъюнктом.

LaTeX

$$$\mathrm{unitizationStarAlgEquiv} : \mathrm{Unitization}\;R\;s \simeq_\star \mathrm{StarAlgebra.adjoin}\;R\,(s)$$$

Lean4

theorem of_algebraMap_eq [Algebra R A] (h : ∀ x, algebraMap R A x = algebraMap S A (algebraMap R S x)) :
    IsScalarTower R S A :=
  ⟨fun x y z => by simp_rw [Algebra.smul_def, RingHom.map_mul, mul_assoc, h]⟩

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