@[reducible, inline]

noncomputable abbrev EuclideanSpace.l1Norm {ι : Type u_1} [Fintype ι] (x : EuclideanSpace ℝ ι) : ℝ

The Euclidean ℓ¹ norm on a finite product, specializing to ℝ^n when ι = Fin n.

@[simp]

theorem EuclideanSpace.l1Norm_eq_sum_abs {ι : Type u_1} [Fintype ι] (x : EuclideanSpace ℝ ι) : ‖x‖₁ = ∑ i : ι, |x.ofLp i|

The Euclidean ℓ¹ norm is the finite sum of the coordinate absolute values.

def «term‖_‖₁» : Lean.ParserDescr

Textbook notation for the Euclidean ℓ¹ norm on a finite product.