instIsBalanced_1 — Mathlib

English

An anisotropic RootPairing is balanced, meaning both pairs (rootSpan, kerRootForm) and (corootSpan, kerCorootForm) are perfect complements.

Русский

Анизотропная парировка корней сбалансирована: пары (rootSpan, kerRootForm) и (corootSpan, kerCorootForm) образуют совершенные дополнения.

LaTeX

$$(P.rootSpan R) ⊕ ker P.RootForm = M \\ \\&\\ (P.corootSpan R) ⊕ ker P.CorootForm = N$$

Lean4

instance : P.IsBalanced where
  isPerfectCompl :=
    { isCompl_left := by simpa only [ker_rootForm_eq_dualAnnihilator] using P.isCompl_rootSpan_ker_rootForm
      isCompl_right := by simpa only [ker_corootForm_eq_dualAnnihilator] using P.isCompl_corootSpan_ker_corootForm }

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