Theorems · Definition · number theory

NumberField.mixedEmbedding.norm

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

The norm of x is ∏ w, (normAtPlace x) ^ mult w. It 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 ℚ, see norm_eq_norm.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

46 results in Mathlib

Foundations

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

Assumes

FieldNumberField