basisDivisor_add_symm — Mathlib

English

For distinct x, y in the field, basisDivisor x y + basisDivisor y x = 1.

Русский

Для x ≠ y в поле, basisDivisor(x,y) + basisDivisor(y,x) = 1.

LaTeX

$$\basisDivisor x y + basisDivisor y x = 1 \quad (x \neq y)$$

Lean4

theorem basisDivisor_add_symm {x y : F} (hxy : x ≠ y) : basisDivisor x y + basisDivisor y x = 1 := by
  classical
    rw [← sum_basis Function.injective_id.injOn ⟨x, mem_insert_self _ { y }⟩, sum_insert (notMem_singleton.mpr hxy),
    sum_singleton, basis_pair_left hxy, basis_pair_right hxy, id, id]

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