mathlib3 documentation

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 #

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
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