norm_eq' — Mathlib

English

For p > 0 and x ∈ ℝ, there is an alternative expression: ‖(x : AddCircle p)‖ = p · | p⁻¹ x − round(p⁻¹ x) |.

Русский

При p > 0 существует альтернативное выражение: ‖(x : AddCircle p)‖ = p · | p⁻¹ x − round(p⁻¹ x) |.

LaTeX

$$$$\\| (x : \\mathrm{AddCircle}(p)) \\| = p \\cdot \\left| p^{-1} x - \\operatorname{round}(p^{-1} x) \\right|.$$$$

Lean4

theorem norm_eq' (hp : 0 < p) {x : ℝ} : ‖(x : AddCircle p)‖ = p * |p⁻¹ * x - round (p⁻¹ * x)| :=
  by
  conv_rhs =>
    congr
    rw [← abs_eq_self.mpr hp.le]
  rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]

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