# mathlib3documentation

number_theory.number_field.canonical_embedding

# Canonical embedding of a number field #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The canonical embedding of a number field K of signature (r₁, r₂) is the ring homomorphism K →+* ℝ^r₁ × ℂ^r₂ that sends x ∈ K to (φ_₁(x),...,φ_r₁(x)) × (ψ_₁(x),..., ψ_r₂(x)) where φ_₁,...,φ_r₁ are its real embeddings and ψ_₁,..., ψ_r₂ are its complex embeddings (up to complex conjugation).

## Main definitions and results #

• number_field.canonical_embedding.ring_of_integers.inter_ball_finite: the intersection of the image of the ring of integers by the canonical embedding and any ball centered at 0 of finite radius is finite.

## Tags #

number field, infinite places

noncomputable def number_field.canonical_embedding (K : Type u_1) [field K] :
K →+* ({w // w.is_real} ) × ({w // w.is_complex} )

The canonical embedding of a number field K of signature (r₁, r₂) into ℝ^r₁ × ℂ^r₂.

Equations
@[simp]
theorem number_field.canonical_embedding.apply_at_real_infinite_place {K : Type u_1} [field K] (w : {w // w.is_real}) (x : K) :
@[simp]
theorem number_field.canonical_embedding.nnnorm_eq {K : Type u_1} [field K] [number_field K] (x : K) :
= finset.univ.sup (λ (w : , w x, _⟩)
theorem number_field.canonical_embedding.norm_le_iff {K : Type u_1} [field K] [number_field K] (x : K) (r : ) :
(w : , w x r
noncomputable def number_field.canonical_embedding.integer_lattice (K : Type u_1) [field K] :
subring (({w // w.is_real} ) × ({w // w.is_complex} ))

The image of 𝓞 K as a subring of ℝ^r₁ × ℂ^r₂.

Equations
Instances for ↥number_field.canonical_embedding.integer_lattice

The linear equiv between 𝓞 K and the integer lattice.

Equations
@[protected, instance]