mul_add_mul — Mathlib

English

In a Boolean ring, a·b + b·a = 0 for all a,b.

Русский

В булевом кольце a·b + b·a = 0 для всех a,b.

LaTeX

$$$$ a\\cdot b + b\\cdot a = 0. $$$$

Lean4

@[simp]
theorem mul_add_mul : a * b + b * a = 0 :=
  by
  have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel
  rwa [left_eq_add] at this

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