eq_mul_inverse_iff_mul_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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