inv_mul_eq_one_of_isUnit — Mathlib

English

For a unit a in ZMod n, a⁻¹ · b = 1 if and only if a = b.

Русский

Для единицы a в ZMod n верно, что a⁻¹ · b = 1 тогда и только тогда, когда a = b.

LaTeX

$$$a^{-1} \cdot b = 1 \iff a = b$ (для единицы $a$)$$

Lean4

theorem inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) : a⁻¹ * b = 1 ↔ a = b := by
  -- ideally, this would be `ha.inv_mul_eq_one`, but `ZMod n` is not a `DivisionMonoid`...
    -- (see the "TODO" above)

  refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
  apply_fun (a * ·) at H
  rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

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