Commit 2024-04-22 09:41 f4476bd4
View on Github →feat: Add mixedEmbedding.norm (#12249)
Define a norm of the mixed space ℝ^r₁ × ℂ^r₂ associated to a number field K of signature (r₁, r₂). The norm is defined such that the norm of mixedEmbedding K a for a : K is equal to the absolute value of the norm of a
over ℚ.
This norm will be used in a future PR about the quotient of the mixed space by the action of the units of K.