Theorems · Definition · number theory

NumberField.mixedEmbedding.convexBodySumFun

{K : Type u_1} → [inst : Field K] → [NumberField K] → NumberField.mixedEmbedding.mixedSpace K → ℝ

The function that sends x : mixedSpace K to ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖. It defines a norm and it used to define convexBodySum.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Cited by

14 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField