isUnit_of_associated_mul — Mathlib

English

If p*b is associated to p and p ≠ 0, then b is a unit.

Русский

Если p·b ассоциировано с p и p ≠ 0, то b — единица.

LaTeX

$$Associated(p*b, p) \land p \neq 0 \rightarrow IsUnit(b)$$

Lean4

theorem isUnit_of_associated_mul [CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p) (hp : p ≠ 0) :
    IsUnit b := by
  obtain ⟨a, ha⟩ := h
  refine isUnit_of_mul_eq_one b a ((mul_right_inj' hp).mp ?_)
  rwa [← mul_assoc, mul_one]

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