eq_of_mul_eq_add_eq_one — Mathlib

English

Let R be a non-associative semiring. If a,b,c ∈ R satisfy a·b = c·a, a + b = 1, and a + c = 1, then b = c.

Русский

Пусть R — полуколь без ассоциативности. Пусть a,b,c ∈ R удовлетворяют a b = c a, a + b = 1 и a + c = 1. Тогда b = c.

LaTeX

$$$a b = c a \quad a + b = 1 \quad a + c = 1 \quad \Rightarrow \quad b = c$$$

Lean4

theorem eq_of_mul_eq_add_eq_one [NonAssocSemiring R] (a : R) {b c : R} (mul : a * b = c * a) (add_ab : a + b = 1)
    (add_ac : a + c = 1) : b = c :=
  calc
    b = (a + c) * b := by rw [add_ac, one_mul]
    _ = c * (a + b) := by rw [add_mul, mul, mul_add]
    _ = c := by rw [add_ab, mul_one]

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