apply_root_root_zero_iff — Mathlib

English

For IsDomain R and NeZero 2, B.form (P.root i) (P.root j) = 0 iff P.pairing i j = 0.

Русский

Пусть R — доменная зона, 2 не нуль; тогда B.form (P.root i) (P.root j) = 0 эквивалентно P.pairing i j = 0.

LaTeX

$$$ B.form\\bigl(P.root\\ i\\bigr)\\bigl(P.root\\ j\\bigr) = 0 \\iff P.pairing\\ i\\ j = 0 $$$

Lean4

@[simp]
theorem apply_root_root_zero_iff [IsDomain R] [NeZero (2 : R)] : B.form (P.root i) (P.root j) = 0 ↔ P.pairing i j = 0 :=
  by
  calc
    B.form (P.root i) (P.root j) = 0 ↔ 2 * B.form (P.root i) (P.root j) = 0 := by simp [two_ne_zero]
    _ ↔ P.pairing i j * B.form (P.root j) (P.root j) = 0 := by rw [B.two_mul_apply_root_root i j]
    _ ↔ P.pairing i j = 0 := by simp [B.ne_zero j]

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