algHomEquivAlgHomOfSplits_apply_apply

English

The action of the Splits-based equivalence preserves evaluation at x.

Русский

Действие эквививалентности на основе разрывов сохраняет вычисление в x.

LaTeX

$$$\\text{algHomEquivAlgHomOfSplits_A L hL f x} = \\text{algebraMap}_L A (f x)$$$

Lean4

theorem algHomEquivAlgHomOfSplits_apply_apply (L : IntermediateField F A)
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
    algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x) :=
  rfl

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