coroot'In_rootSpanMem_eq_pairingIn

English

For Module S M with IsScalarTower and FaithfulSMul, and P valued in S, root'In S i (corootSpanMem S j) equals pairingIn S i j.

Русский

При модуле S M и условиях IsScalarTower, FaithfulSMul, P ценованного в S, имеем root'In S i (corootSpanMem S j) = pairingIn S i j.

LaTeX

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

Lean4

@[simp]
theorem coroot'In_rootSpanMem_eq_pairingIn [Module S M] [IsScalarTower S R M] [FaithfulSMul S R] [P.IsValuedIn S] :
    P.coroot'In S i (P.rootSpanMem S j) = P.pairingIn S j i :=
  rfl

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