inv_mul_eq_inv_mul_iff — Mathlib

English

Let b,d be units. Then b^{-1}·a = d^{-1}·c if and only if a·d = c·b.

Русский

Пусть b,d — единицы. Тогда b^{-1}·a = d^{-1}·c тогда и только тогда, когда a·d = c·b.

LaTeX

$$$$ \\forall b,d \\in \\alpha^{\\times},\\ a,b,c,d \\in \\alpha:\\ b^{-1} a = d^{-1} c \\iff a d = c b. $$$$

Lean4

@[to_additive]
protected theorem inv_mul_eq_inv_mul_iff (hb : IsUnit b) (hd : IsUnit d) : b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b := by
  rw [← div_eq_inv_mul, ← div_eq_inv_mul, hb.div_eq_div_iff hd]

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