norm_neg_period — Mathlib

English

The norm on AddCircle (−p) equals the norm on AddCircle (p); i.e., the norm is invariant under sign change of p.

Русский

Норма на AddCircle (−p) равна норме на AddCircle (p); тождество нормы при смене знака p.

LaTeX

$$$$\\| (x : \\mathrm{AddCircle}(-p)) \\| = \\| (x : \\mathrm{AddCircle}(p)) \\|.$$$$

Lean4

theorem norm_neg_period (x : ℝ) : ‖(x : AddCircle (-p))‖ = ‖(x : AddCircle p)‖ :=
  by
  suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖
    by
    rw [← this, neg_one_mul]
    simp
  simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

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