root'_apply_apply_mem_of_mem_span

English

For Module S N with IsScalarTower and FaithfulSMul and P.IsValuedIn S, we have P.root'In S i (P.corootSpanMem S j) = P.pairingIn S i j.

Русский

При любых условиях модуля S N и свойств P IsValuedIn S имеем P.root'In S i (P.corootSpanMem S j) = P.pairingIn S i j.

LaTeX

$$$P.root'In\;S\;i\;(P.corootSpanMem\;S\;j) = P.pairingIn\;S\;i\;j$$$

Lean4

theorem root'_apply_apply_mem_of_mem_span [Module S N] [IsScalarTower S R N] [P.IsValuedIn S] {x : N}
    (hx : x ∈ span S (range P.coroot)) (i : ι) : P.root' i x ∈ LinearMap.range (Algebra.linearMap S R) :=
  P.flip.coroot'_apply_apply_mem_of_mem_span S hx i

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