# Embeddings of number fields #

This file defines the embeddings of a number field into an algebraic closed field.

## Main Definitions and Results #

• NumberField.Embeddings.range_eval_eq_rootSet_minpoly: let x ∈ K with K number field and let A be an algebraic closed field of char. 0, then the images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.
• NumberField.Embeddings.pow_eq_one_of_norm_eq_one: an algebraic integer whose conjugates are all of norm one is a root of unity.
• NumberField.InfinitePlace: the type of infinite places of a number field K.
• NumberField.InfinitePlace.mk_eq_iff: two complex embeddings define the same infinite place iff they are equal or complex conjugates.
• NumberField.InfinitePlace.prod_eq_abs_norm: the infinite part of the product formula, that is for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where the product is over the infinite place w and ‖·‖_w is the normalized absolute value for w.

## Tags #

number field, embeddings, places, infinite places

noncomputable instance NumberField.Embeddings.instFintypeRingHom (K : Type u_1) [] [] (A : Type u_2) [] [] :

There are finitely many embeddings of a number field.

Equations
theorem NumberField.Embeddings.card (K : Type u_1) [] [] (A : Type u_2) [] [] [] :

The number of embeddings of a number field is equal to its finrank.

instance NumberField.Embeddings.instNonemptyRingHom (K : Type u_1) [] [] (A : Type u_2) [] [] [] :
Equations
• =
theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly (K : Type u_1) (A : Type u_2) [] [] [] [] [] (x : K) :
(Set.range fun (φ : K →+* A) => φ x) = ().rootSet A

Let A be an algebraically closed field and let x ∈ K, with K a number field. The images of x by the embeddings of K in A are exactly the roots in A of the minimal polynomial of x over ℚ.

theorem NumberField.Embeddings.coeff_bdd_of_norm_le {K : Type u_1} [] [] {A : Type u_2} [] [] [] {B : } {x : K} (h : ∀ (φ : K →+* A), φ x B) (i : ) :
().coeff i * (.choose ())
theorem NumberField.Embeddings.finite_of_norm_le (K : Type u_1) [] [] (A : Type u_2) [] [] [] (B : ) :
{x : K | ∀ (φ : K →+* A), φ x B}.Finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one (K : Type u_1) [] [] (A : Type u_2) [] [] [] {x : K} (hxi : ) (hx : ∀ (φ : K →+* A), φ x = 1) :
∃ (n : ) (_ : 0 < n), x ^ n = 1

An algebraic integer whose conjugates are all of norm one is a root of unity.

def NumberField.place {K : Type u_1} [] {A : Type u_2} [] (φ : K →+* A) :

An embedding into a normed division ring defines a place of K

Equations
• = .comp
Instances For
@[simp]
theorem NumberField.place_apply {K : Type u_1} [] {A : Type u_2} [] (φ : K →+* A) (x : K) :
x = φ x
@[reducible, inline]

The conjugate of a complex embedding as a complex embedding.

Equations
Instances For
@[simp]
theorem NumberField.ComplexEmbedding.conjugate_coe_eq {K : Type u_1} [] (φ : K →+* ) (x : K) :
= () (φ x)
@[reducible, inline]
abbrev NumberField.ComplexEmbedding.IsReal {K : Type u_1} [] (φ : K →+* ) :

An embedding into ℂ is real if it is fixed by complex conjugation.

Equations
Instances For

A real embedding as a ring homomorphism from K to ℝ .

Equations
• .embedding = { toFun := fun (x : K) => (φ x).re, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply {K : Type u_1} [] {φ : K →+* } (x : K) :
(.embedding x) = φ x
theorem NumberField.ComplexEmbedding.IsReal.comp {K : Type u_1} [] {k : Type u_2} [] (f : k →+* K) {φ : K →+* } :
theorem NumberField.ComplexEmbedding.isReal_comp_iff {K : Type u_1} [] {k : Type u_2} [] {f : k ≃+* K} {φ : K →+* } :
theorem NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] [IsGalois k K] (φ : K →+* ) (ψ : K →+* ) (h : φ.comp () = ψ.comp ()) :
∃ (σ : K ≃ₐ[k] K), φ.comp σ.symm = ψ
def NumberField.ComplexEmbedding.IsConj {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] (φ : K →+* ) (σ : K ≃ₐ[k] K) :

IsConj φ σ states that σ : K ≃ₐ[k] K is the conjugation under the embedding φ : K →+* ℂ.

Equations
• = ( = φ.comp σ)
Instances For
theorem NumberField.ComplexEmbedding.IsConj.eq {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} (h : ) (x : K) :
φ (σ x) = star (φ x)
theorem NumberField.ComplexEmbedding.IsConj.ext {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ₁ : K ≃ₐ[k] K} {σ₂ : K ≃ₐ[k] K} (h₁ : ) (h₂ : ) :
σ₁ = σ₂
theorem NumberField.ComplexEmbedding.IsConj.ext_iff {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ₁ : K ≃ₐ[k] K} {σ₂ : K ≃ₐ[k] K} (h₁ : ) :
σ₁ = σ₂
theorem NumberField.ComplexEmbedding.IsConj.isReal_comp {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} (h : ) :
theorem NumberField.ComplexEmbedding.isConj_one_iff {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } :
theorem NumberField.ComplexEmbedding.IsReal.isConjGal_one {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } :

Alias of the reverse direction of NumberField.ComplexEmbedding.isConj_one_iff.

theorem NumberField.ComplexEmbedding.IsConj.symm {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} (hσ : ) :
theorem NumberField.ComplexEmbedding.isConj_symm {K : Type u_1} [] {k : Type u_2} [] [Algebra k K] {φ : K →+* } {σ : K ≃ₐ[k] K} :
def NumberField.InfinitePlace (K : Type u_2) [] :
Type u_2

An infinite place of a number field K is a place associated to a complex embedding.

Equations
Instances For
instance instNonemptyInfinitePlaceOfNumberField (K : Type u_2) [] [] :
Equations
• =
noncomputable def NumberField.InfinitePlace.mk {K : Type u_2} [] (φ : K →+* ) :

Return the infinite place defined by a complex embedding φ.

Equations
Instances For
Equations
• NumberField.InfinitePlace.instFunLikeReal = { coe := fun (w : ) (x : K) => w x, coe_injective' := }
Equations
• =
@[simp]
theorem NumberField.InfinitePlace.apply {K : Type u_2} [] (φ : K →+* ) (x : K) :
= Complex.abs (φ x)
noncomputable def NumberField.InfinitePlace.embedding {K : Type u_2} [] (w : ) :

For an infinite place w, return an embedding φ such that w = infinite_place φ .

Equations
• w.embedding = .choose
Instances For
@[simp]
@[simp]
theorem NumberField.InfinitePlace.norm_embedding_eq {K : Type u_2} [] (w : ) (x : K) :
w.embedding x = w x
theorem NumberField.InfinitePlace.eq_iff_eq {K : Type u_2} [] (x : K) (r : ) :
(∀ (w : ), w x = r) ∀ (φ : K →+* ), φ x = r
theorem NumberField.InfinitePlace.le_iff_le {K : Type u_2} [] (x : K) (r : ) :
(∀ (w : ), w x r) ∀ (φ : K →+* ), φ x r
theorem NumberField.InfinitePlace.pos_iff {K : Type u_2} [] {w : } {x : K} :
0 < w x x 0
@[simp]
theorem NumberField.InfinitePlace.mk_eq_iff {K : Type u_2} [] {φ : K →+* } {ψ : K →+* } :
def NumberField.InfinitePlace.IsReal {K : Type u_2} [] (w : ) :

An infinite place is real if it is defined by a real embedding.

Equations
Instances For

An infinite place is complex if it is defined by a complex (ie. not real) embedding.

Equations
Instances For
theorem NumberField.InfinitePlace.embedding_mk_eq {K : Type u_2} [] (φ : K →+* ) :
.embedding = φ
@[simp]
theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal {K : Type u_2} [] {φ : K →+* } :
.embedding = φ
@[simp]
theorem NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal {K : Type u_2} [] {w : } (h : w.IsReal) :
@[simp]
theorem NumberField.InfinitePlace.not_isReal_iff_isComplex {K : Type u_2} [] {w : } :
¬w.IsReal w.IsComplex
@[simp]
theorem NumberField.InfinitePlace.not_isComplex_iff_isReal {K : Type u_2} [] {w : } :
¬w.IsComplex w.IsReal
theorem NumberField.InfinitePlace.isReal_or_isComplex {K : Type u_2} [] (w : ) :
w.IsReal w.IsComplex
theorem NumberField.InfinitePlace.ne_of_isReal_isComplex {K : Type u_2} [] {w : } {w' : } (h : w.IsReal) (h' : w'.IsComplex) :
w w'
theorem NumberField.InfinitePlace.disjoint_isReal_isComplex (K : Type u_2) [] :
Disjoint {w : | w.IsReal} {w : | w.IsComplex}
noncomputable def NumberField.InfinitePlace.embedding_of_isReal {K : Type u_2} [] {w : } (hw : w.IsReal) :

The real embedding associated to a real infinite place.

Equations
• = .embedding
Instances For
@[simp]
theorem NumberField.InfinitePlace.embedding_of_isReal_apply {K : Type u_2} [] {w : } (hw : w.IsReal) (x : K) :
= w.embedding x
theorem NumberField.InfinitePlace.norm_embedding_of_isReal {K : Type u_2} [] {w : } (hw : w.IsReal) (x : K) :
@[simp]
theorem NumberField.InfinitePlace.isReal_of_mk_isReal {K : Type u_2} [] {φ : K →+* } (h : .IsReal) :
@[simp]
theorem NumberField.InfinitePlace.not_isReal_of_mk_isComplex {K : Type u_2} [] {φ : K →+* } (h : .IsComplex) :
noncomputable def NumberField.InfinitePlace.mult {K : Type u_2} [] (w : ) :

The multiplicity of an infinite place, that is the number of distinct complex embeddings that define it, see card_filter_mk_eq.

Equations
• w.mult = if w.IsReal then 1 else 2
Instances For
theorem NumberField.InfinitePlace.card_filter_mk_eq {K : Type u_2} [] [] (w : ) :
(Finset.filter (fun (φ : K →+* ) => ) Finset.univ).card = w.mult
noncomputable instance NumberField.InfinitePlace.NumberField.InfinitePlace.fintype {K : Type u_2} [] [] :
Equations
theorem NumberField.InfinitePlace.sum_mult_eq {K : Type u_2} [] [] :
(Finset.univ.sum fun (w : ) => w.mult) =
noncomputable def NumberField.InfinitePlace.mkReal {K : Type u_2} [] :
{ φ : K →+* // } { w : // w.IsReal }

The map from real embeddings to real infinite places as an equiv

Equations
Instances For
noncomputable def NumberField.InfinitePlace.mkComplex {K : Type u_2} [] :
{ φ : K →+* // }{ w : // w.IsComplex }

The map from nonreal embeddings to complex infinite places

Equations
• NumberField.InfinitePlace.mkComplex = Subtype.map NumberField.InfinitePlace.mk
Instances For
@[simp]
theorem NumberField.InfinitePlace.mkReal_coe {K : Type u_2} [] (φ : { φ : K →+* // }) :
(NumberField.InfinitePlace.mkReal φ) =
@[simp]
theorem NumberField.InfinitePlace.mkComplex_coe {K : Type u_2} [] (φ : { φ : K →+* // }) :
theorem NumberField.InfinitePlace.prod_eq_abs_norm {K : Type u_2} [] [] (x : K) :
(Finset.univ.prod fun (w : ) => w x ^ w.mult) = | x|

The infinite part of the product formula : for x ∈ K, we have Π_w ‖x‖_w = |norm(x)| where ‖·‖_w is the normalized absolute value for w.

theorem NumberField.InfinitePlace.one_le_of_lt_one {K : Type u_2} [] [] {w : } {a : } (ha : a 0) (h : ∀ ⦃z : ⦄, z wz a < 1) :
1 w a
theorem NumberField.is_primitive_element_of_infinitePlace_lt {K : Type u_2} [] [] {x : } {w : } (h₁ : x 0) (h₂ : ∀ ⦃w' : ⦄, w' ww' x < 1) (h₃ : w.IsReal |(w.embedding x).re| < 1) :
x =
theorem NumberField.adjoin_eq_top_of_infinitePlace_lt {K : Type u_2} [] [] {x : } {w : } (h₁ : x 0) (h₂ : ∀ ⦃w' : ⦄, w' ww' x < 1) (h₃ : w.IsReal |(w.embedding x).re| < 1) :
@[reducible, inline]
noncomputable abbrev NumberField.InfinitePlace.NrRealPlaces (K : Type u_2) [] [] :

The number of infinite real places of the number field K.

Equations
Instances For
@[reducible, inline]
noncomputable abbrev NumberField.InfinitePlace.NrComplexPlaces (K : Type u_2) [] [] :

The number of infinite complex places of the number field K.

Equations
Instances For
def NumberField.InfinitePlace.comap {k : Type u_1} [] {K : Type u_2} [] (w : ) (f : k →+* K) :

The restriction of an infinite place along an embedding.

Equations
• w.comap f = (w).comp ,
Instances For
@[simp]
theorem NumberField.InfinitePlace.comap_mk {k : Type u_1} [] {K : Type u_2} [] (φ : K →+* ) (f : k →+* K) :
.comap f = NumberField.InfinitePlace.mk (φ.comp f)
theorem NumberField.InfinitePlace.comap_id {K : Type u_2} [] (w : ) :
w.comap () = w
theorem NumberField.InfinitePlace.comap_comp {k : Type u_1} [] {K : Type u_2} [] {F : Type u_3} [] (w : ) (f : F →+* K) (g : k →+* F) :
w.comap (f.comp g) = (w.comap f).comap g
theorem NumberField.InfinitePlace.IsReal.comap {k : Type u_1} [] {K : Type u_2} [] (f : k →+* K) {w : } (hφ : w.IsReal) :
(w.comap f).IsReal
theorem NumberField.InfinitePlace.isReal_comap_iff {k : Type u_1} [] {K : Type u_2} [] (f : k ≃+* K) {w : } :
(w.comap f).IsReal w.IsReal
theorem NumberField.InfinitePlace.comap_surjective {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [] :
Function.Surjective fun (x : ) => x.comap ()
theorem NumberField.InfinitePlace.mult_comap_le {k : Type u_1} [] {K : Type u_2} [] (f : k →+* K) (w : ) :
(w.comap f).mult w.mult
theorem NumberField.InfinitePlace.card_mono (k : Type u_1) [] (K : Type u_2) [] [Algebra k K] [] [] :
@[simp]
theorem NumberField.InfinitePlace.instMulActionAlgEquiv_smul_coe_apply {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] (σ : K ≃ₐ[k] K) (w : ) :
∀ (a : K), () a = w (σ.symm a)
instance NumberField.InfinitePlace.instMulActionAlgEquiv {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] :

The action of the galois group on infinite places.

Equations
• NumberField.InfinitePlace.instMulActionAlgEquiv =
theorem NumberField.InfinitePlace.smul_eq_comap {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] (σ : K ≃ₐ[k] K) (w : ) :
σ w = w.comap σ.symm
@[simp]
theorem NumberField.InfinitePlace.smul_apply {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] (σ : K ≃ₐ[k] K) (w : ) (x : K) :
(σ w) x = w (σ.symm x)
@[simp]
theorem NumberField.InfinitePlace.smul_mk {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] (σ : K ≃ₐ[k] K) (φ : K →+* ) :
= NumberField.InfinitePlace.mk (φ.comp σ.symm)
theorem NumberField.InfinitePlace.comap_smul {k : Type u_1} [] {K : Type u_2} [] {F : Type u_3} [] [Algebra k K] (σ : K ≃ₐ[k] K) (w : ) {f : F →+* K} :
(σ w).comap f = w.comap ((σ.symm).comp f)
theorem NumberField.InfinitePlace.isReal_smul_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {σ : K ≃ₐ[k] K} {w : } :
(σ w).IsReal w.IsReal
theorem NumberField.InfinitePlace.isComplex_smul_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {σ : K ≃ₐ[k] K} {w : } :
(σ w).IsComplex w.IsComplex
theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] (φ : K →+* ) (ψ : K →+* ) (h : φ.comp () = ψ.comp ()) :
∃ (σ : K ≃ₐ[k] K), φ.comp σ.symm = ψ
theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] {w : } {w' : } (h : w.comap () = w'.comap ()) :
∃ (σ : K ≃ₐ[k] K), σ w = w'
theorem NumberField.InfinitePlace.mem_orbit_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] {w : } {w' : } :
w' MulAction.orbit (K ≃ₐ[k] K) w w.comap () = w'.comap ()
noncomputable def NumberField.InfinitePlace.orbitRelEquiv {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] :

The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.

Equations
Instances For
theorem NumberField.InfinitePlace.orbitRelEquiv_apply_mk'' {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] (w : ) :
NumberField.InfinitePlace.orbitRelEquiv () = w.comap ()
def NumberField.InfinitePlace.IsUnramified (k : Type u_1) [] {K : Type u_2} [] [Algebra k K] (w : ) :

An infinite place is unramified in a field extension if the restriction has the same multiplicity.

Equations
• = ((w.comap ()).mult = w.mult)
Instances For
theorem NumberField.InfinitePlace.IsUnramified.eq {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } :
(w.comap ()).mult = w.mult
theorem NumberField.InfinitePlace.isUnramified_iff_mult_le {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } :
w.mult (w.comap ()).mult
theorem NumberField.InfinitePlace.IsUnramified.comap_algHom {k : Type u_1} [] {K : Type u_2} [] {F : Type u_3} [] [Algebra k K] [Algebra k F] {w : } (f : K →ₐ[k] F) :
theorem NumberField.InfinitePlace.IsUnramified.of_restrictScalars {k : Type u_1} [] (K : Type u_2) [] {F : Type u_3} [] [Algebra k K] [Algebra k F] [Algebra K F] [] {w : } :
theorem NumberField.InfinitePlace.IsUnramified.comap {k : Type u_1} [] (K : Type u_2) [] {F : Type u_3} [] [Algebra k K] [Algebra k F] [Algebra K F] [] {w : } :
theorem NumberField.InfinitePlace.not_isUnramified_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } :
w.IsComplex (w.comap ()).IsReal
theorem NumberField.InfinitePlace.isUnramified_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } :
w.IsReal (w.comap ()).IsComplex
theorem NumberField.InfinitePlace.IsReal.isUnramified (k : Type u_1) [] {K : Type u_2} [] [Algebra k K] {w : } (h : w.IsReal) :
theorem NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* } (h : ) :
theorem NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] {φ : K →+* } :
∀ (σ : K ≃ₐ[k] K), σ = 1
theorem NumberField.InfinitePlace.mem_stabilizer_mk_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] (φ : K →+* ) (σ : K ≃ₐ[k] K) :
σ
theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* } (h : ) :
() = {1, σ}
theorem NumberField.InfinitePlace.card_stabilizer {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } [IsGalois k K] :
Nat.card (MulAction.stabilizer (K ≃ₐ[k] K) w) = if then 1 else 2
theorem NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } [IsGalois k K] (hw : ) :
theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } [IsGalois k K] [] (hw : ) :
theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramified {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {w : } [IsGalois k K] (hw : ) :
theorem NumberField.InfinitePlace.isUnramified_smul_iff {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] {σ : K ≃ₐ[k] K} {w : } :
def NumberField.InfinitePlace.IsUnramifiedIn {k : Type u_1} [] (K : Type u_2) [] [Algebra k K] (w : ) :

A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.

Equations
• = ∀ (v : ), v.comap () = w
Instances For
theorem NumberField.InfinitePlace.card_isUnramified (k : Type u_1) [] (K : Type u_2) [] [] [Algebra k K] [] [IsGalois k K] :
(Finset.filter Finset.univ).card = (Finset.filter Finset.univ).card *
theorem NumberField.InfinitePlace.card_isUnramified_compl (k : Type u_1) [] (K : Type u_2) [] [] [Algebra k K] [] [IsGalois k K] :
(Finset.filter Finset.univ).card = (Finset.filter Finset.univ).card * ()
theorem NumberField.InfinitePlace.card_eq_card_isUnramifiedIn (k : Type u_1) [] (K : Type u_2) [] [] [Algebra k K] [] [IsGalois k K] :
= (Finset.filter Finset.univ).card * + (Finset.filter Finset.univ).card * ()
class IsUnramifiedAtInfinitePlaces (k : Type u_1) [] (K : Type u_2) [] [Algebra k K] :

A field extension is unramified at infinite places if every infinite place is unramified.

• isUnramified :
Instances
theorem IsUnramifiedAtInfinitePlaces.isUnramified {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [self : ] (w : ) :
instance IsUnramifiedAtInfinitePlaces.id (K : Type u_2) [] :
Equations
• =
theorem IsUnramifiedAtInfinitePlaces.trans (k : Type u_1) [] (K : Type u_2) [] (F : Type u_3) [] [Algebra k K] [Algebra k F] [Algebra K F] [] [h₁ : ] [h₂ : ] :
theorem IsUnramifiedAtInfinitePlaces.top (k : Type u_1) [] (K : Type u_2) [] (F : Type u_3) [] [Algebra k K] [Algebra k F] [Algebra K F] [] [h : ] :
theorem IsUnramifiedAtInfinitePlaces.bot (k : Type u_1) [] (K : Type u_2) [] (F : Type u_3) [] [Algebra k K] [Algebra k F] [Algebra K F] [] [h₁ : ] [] :
theorem NumberField.InfinitePlace.isUnramified (k : Type u_1) [] {K : Type u_2} [] [Algebra k K] (w : ) :
theorem NumberField.InfinitePlace.isUnramifiedIn {k : Type u_1} [] (K : Type u_2) [] [Algebra k K] (w : ) :
theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] [] (h : Odd (Fintype.card (K ≃ₐ[k] K))) :
theorem IsUnramifiedAtInfinitePlaces_of_odd_finrank {k : Type u_1} [] {K : Type u_2} [] [Algebra k K] [IsGalois k K] (h : ) :
theorem IsUnramifiedAtInfinitePlaces.card_infinitePlace (k : Type u_1) [] (K : Type u_2) [] [Algebra k K] [] [] [IsGalois k K] :
theorem IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt {K : Type u_1} [] [] {ζ : K} {k : } (hk : 2 < k) (hζ : ) :