Commit 2024-06-03 10:24 d7fd3e43

feat(NumberField/CanonicalEmbedding): add normAtPlace (#13135) Working in the mixed space ℝ^r₁ × ℂ^r₂ associated to a number field can be sometimes tedious since one has to deal separately with real and complex components even though the arguments are often very similar. In order to make working with norms easier, this PR defines for an infinite place w and an element x of ℝ^r₁ × ℂ^r₂, normAtPlace w x as essentially ‖x w‖ and proves many properties about it. This make it possible to golf some existing proofs and will also make things simpler in the coming PRs about the fundamental cone.