inverse_mul_eq_iff_eq_mul — Mathlib

English

Let x be a unit and y,z arbitrary. Then x^{-1} · y = z if and only if y = x · z.

Русский

Пусть x является единицей. Тогда x^{-1} · y = z тогда и только тогда, когда y = x · z.

LaTeX

$$$\forall x,y,z\,\text{IsUnit}(x) \Rightarrow (x^{-1}\cdot y = z) \iff (y = x\cdot z)$$$

Lean4

theorem inverse_mul_eq_iff_eq_mul (x y z : M₀) (h : IsUnit x) : inverse x * y = z ↔ y = x * z :=
  ⟨fun h1 => by rw [← h1, mul_inverse_cancel_left _ _ h], fun h1 => by rw [h1, inverse_mul_cancel_left _ _ h]⟩

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