OAI/NumberTheory/DukePrimeDegree/Arithmetic/ExceptionalUniverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting exceptional-zero exclusion between universes

Every ordered totally real number field embeds in the real numbers. Its image is a small isomorphic number field with the same discriminant and continued zeta zero orders. Thus a Type-level class-field theorem suffices for the universe-polymorphic main statement.

  1. theorem OAI.DukePrimeDegree.exceptionalRealZeroExclusion_lift line 23