Positivity in the narrow ray condition over the rationals
ProvedRat.ringOfIntegers_pos_iff_all_real_embeddingsclass-field-theorynumber-theory
For an algebraic integer of , positivity under every real embedding of is equivalent to positivity of the corresponding integer in . This converts the archimedean condition in the narrow ray subgroup of into the usual positive-generator condition used to identify its ray classes with .
Preamble
import Mathlib.NumberTheory.NumberField.Basic import Mathlib.Data.Real.Basic
Formal statement
theorem Rat.ringOfIntegers_pos_iff_all_real_embeddings (a : NumberField.RingOfIntegers ℚ) :
0 < Rat.ringOfIntegersEquiv a ↔
∀ τ : ℚ →+* ℝ, 0 < τ (algebraMap (NumberField.RingOfIntegers ℚ) ℚ a) := by sorrySource
Mathlib, NumberTheory/NumberField/Basic, Rat.ringOfIntegersEquiv and Rat.ringOfIntegersEquiv_apply_coe, https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/NumberField/Basic.html ; Prove2Me Definitions.Def_NarrowRayClassGroup, definition Deep.NTSupply.narrowRaySet, archimedean positivity conjunct.