eq_of_add_add_eq_zero — Mathlib

English

If B is alternating and a+b+c=0, then B(a,b)=B(b,c).

Русский

Если B чередующаяся и a+b+c=0, тогда B(a,b)=B(b,c).

LaTeX

$$$\text{IsAlt}(B) \Rightarrow \forall a,b,c:\, a+b+c=0 \Rightarrow B(a,b)=B(b,c)$$$

Lean4

theorem eq_of_add_add_eq_zero [IsCancelAdd M] {a b c : M₁} (hAdd : a + b + c = 0) : B a b = B b c :=
  by
  have : B a a + B a b + B a c = B a c + B b c + B c c := by
    simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
  rw [H, H, zero_add, add_zero, add_comm] at this
  exact add_left_cancel this

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