pairing_eq_zero_iff — Mathlib

English

Under NeZero 2 and IsDomain, pairing i j = 0 iff pairing j i = 0.

Русский

При NeZero 2 и IsDomain, pairing i j = 0 эквивалентно 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)] [NoZeroSMulDivisors R M] : P.pairing i j = 0 ↔ P.pairing j i = 0 :=
  by
  suffices ∀ {i j : ι}, P.pairing i j = 0 → P.pairing j i = 0 from ⟨this, this⟩
  intro i j h
  simpa [P.ne_zero i, reflectionPerm_eq_iff_smul_root] using P.reflectionPerm_eq_of_pairing_eq_zero' h

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