neg_add_eq_mul_invOf_mul_same_iff

English

In a ring, for invertible a,b, and a+b invertible, -(b + a) = a * inv(b) * a iff -1 = inv(a) * b + inv(b) * a.

Русский

В кольце для обратимых a,b и обратимого a+b, -(b + a) = a * inv(b) * a эквивалентно -1 = inv(a) * b + inv(b) * a.

LaTeX

$$-(b + a) = a * ⅟b * a \iff -1 = ⅟a * b + ⅟b * a$$

Lean4

theorem neg_add_eq_mul_invOf_mul_same_iff [Ring R] {a b : R} [Invertible a] [Invertible b] :
    -(b + a) = a * ⅟b * a ↔ -1 = ⅟a * b + ⅟b * a :=
  calc
    -(b + a) = a * ⅟b * a ↔ -a = b + a * ⅟b * a := ⟨by grind, fun h ↦ by simp [h]⟩
    _ ↔ -a = a * ⅟a * b + a * ⅟b * a := by rw [mul_invOf_self, one_mul]
    _ ↔ -a = a * (⅟a * b + ⅟b * a) := by simp only [mul_add, mul_assoc]
    _ ↔ -1 = ⅟a * b + ⅟b * a := ⟨fun h ↦ by simpa using congr_arg (⅟a * ·) h, fun h ↦ by simp [← h]⟩

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