isOrthogonal_iff_pairing_eq_zero — Mathlib

English

Let R be a commutative ring with 2 ≠ 0 and M a module over R with NoZeroSMulDivisors. For any indices i, j in ι, the root pairing is orthogonal precisely when the pairing value vanishes: P.IsOrthogonal i j ⇔ P.pairing i j = 0.

Русский

Пусть R — коммутативное кольцо с 2 ≠ 0 и M — модуль над R, удовлетворяющий NoZeroSMulDivisors. Для любых индексов i, j в ι пара корней ортогональна тогда и только тогда, когда значение парирования равно нулю: P.IsOrthogonal i j ⇔ P.pairing i j = 0.

LaTeX

$$$ P^{\\}IsOrthogonal(i,j) \\iff P.pairing(i,j) = 0 $$$

Lean4

theorem isOrthogonal_iff_pairing_eq_zero [NeZero (2 : R)] [NoZeroSMulDivisors R M] :
    P.IsOrthogonal i j ↔ P.pairing i j = 0 :=
  ⟨fun h ↦ h.1, fun h ↦ ⟨h, pairing_eq_zero_iff.mp h⟩⟩

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