algebraMap_coroot'In_apply — Mathlib

English

The algebra map sends coroot'In evaluated on a span element into the base ring.

Русский

Алгебраическое отображение переводит coroot'In на элемент span в исходное кольцо.

LaTeX

$$$\operatorname{algebraMap}_{S\to R}(P.coroot'In\;S i\;x) = P.coroot' i\;x$$$

Lean4

@[simp]
theorem algebraMap_coroot'In_apply [Module S M] [IsScalarTower S R M] [FaithfulSMul S R] [P.IsValuedIn S] (i : ι)
    (x : P.rootSpan S) : algebraMap S R (P.coroot'In S i x) = P.coroot' i x :=
  P.flip.algebraMap_root'In_apply S i x

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