divp_eq_divp_iff — Mathlib

English

For α a commutative monoid, x,y ∈ α and ux, uy ∈ Units α, x /ₚ ux = y /ₚ uy iff x · uy = y · ux.

Русский

Для коммутативного моноида α, x,y ∈ α и ux, uy ∈ Units α, x /ₚ ux = y /ₚ uy тогда и только тогда, когда x · uy = y · ux.

LaTeX

$$$ x /ₚ ux = y /ₚ uy \iff x \cdot uy = y \cdot ux $$$

Lean4

theorem divp_eq_divp_iff {x y : α} {ux uy : αˣ} : x /ₚ ux = y /ₚ uy ↔ x * uy = y * ux := by
  rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

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