algHomEquivAlgHomOfSplits_apply_apply

English

The composition equality between the implemented equiv and algebra maps holds.

Русский

Сохранено равенство композиции реализованной эквиви и алгебраических отображений.

LaTeX

$$$(\\text{equivOfEquiv L M hSR}).toRingHom \\circ (algebraMap S L) = (algebraMap R M) \\circ hSR$$$

Lean4

theorem algHomEquivAlgHomOfSplits_apply_apply (L : Type*) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A]
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
    Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x) :=
  rfl

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