units_div_eq_mul — Mathlib

English

For units u1, u2 ∈ ℤˣ, division is multiplication: u1 / u2 = u1 · u2.

Русский

Для единиц u1, u2 ∈ ℤˣ деление равно умножению: u1 / u2 = u1 · u2.

LaTeX

$$$\forall u_1,u_2 \in \mathbb{Z}^{\times}, \ u_1 / u_2 = u_1 \cdot u_2.$$$

Lean4

theorem units_div_eq_mul (u₁ u₂ : ℤˣ) : u₁ / u₂ = u₁ * u₂ := by
  rw [div_eq_mul_inv, units_inv_eq_self]
    -- `Units.val_mul` is a "wrong turn" for the simplifier, this undoes it and simplifies further

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