of_algebraMap_eq' — Mathlib

English

Applying algebraMap after the tower composition is the same as the direct algebraMap.

Русский

Применение algebraMap после композиции башни равно прямому algebraMap.

LaTeX

$$$\text{algebraMap}\;R\;A\ x = \text{algebraMap}\;S\;A\ (\text{algebraMap}\;R\;S\ x)$$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
theorem of_algebraMap_eq' [Algebra R A] (h : algebraMap R A = (algebraMap S A).comp (algebraMap R S)) :
    IsScalarTower R S A :=
  of_algebraMap_eq <| RingHom.ext_iff.1 h

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