pairing_eq_zero_iff' — Mathlib

English

Similar to the previous lemma: under appropriate hypotheses, pairing i j = 0 iff pairing j i = 0.

Русский

Похожее на предыдущее: при подходящих условиях pairing i j = 0 iff pairing j i = 0.

LaTeX

$$$$ P.pairing(i,j) = 0 \\iff P.pairing(j,i) = 0. $$$$

Lean4

theorem pairing_eq_zero_iff' [NeZero (2 : R)] [IsDomain R] : P.pairing i j = 0 ↔ P.pairing j i = 0 :=
  by
  have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  exact pairing_eq_zero_iff

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