Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone

(K : Type u_1) → [inst : Field K] → [NumberField K] → Set (NumberField.mixedEmbedding.mixedSpace K)

The fundamental cone is a cone in the mixed space, i.e. a subset fixed by multiplication by a nonzero real number, see smul_mem_of_mem, that is also a fundamental domain for the action of (𝓞 K)ˣ modulo torsion, see exists_unit_smul_mem and torsion_smul_mem_of_mem.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

22 results in Mathlib

Foundations

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

Assumes

FieldNumberField