inverse_pow_mul_eq_iff_eq_mul — Mathlib

English

If a is a unit, then for all k, ring.inverse(a)^k * b = c iff b = a^k * c.

Русский

Если a является единицей, тогда для всех k: inverse(a)^k · b = c эквивалентно b = a^k · c.

LaTeX

$$$IsUnit(a) \rightarrow \left( \text{inverse}(a)^k \cdot b = c \iff b = a^k \cdot c \right)$$$

Lean4

theorem inverse_pow_mul_eq_iff_eq_mul {a : M₀} (b c : M₀) (ha : IsUnit a) {k : ℕ} :
    Ring.inverse a ^ k * b = c ↔ b = a ^ k * c := by
  rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]

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