Theorems · Definition · number theory

NumberField.place

{K : Type u_1} → [inst : Field K] → {A : Type u_2} → [inst_1 : NormedDivisionRing A] → (K →+* A) → AbsoluteValue K ℝ

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

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

71 results in Mathlib

Foundations

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

Assumes

FieldNormedDivisionRing