NYLL
Module

SmallModel.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SmallModel
2 declarations indexed from sourceView source ↗

Module documentation

Small models of number fields

A number field has finite dimension over the countable field ℚ, so its underlying type has a representative in the lowest universe. The ring equivalence to that representative preserves the number-field structure.

Imports6
  • Mathlib.Algebra.Field.Shrink
  • Mathlib.Algebra.Ring.Shrink
  • Mathlib.Basic.Countable.Small
  • Mathlib.Data.Rat.Encodable
  • Mathlib.LinearAlgebra.Countable
  • Mathlib.NumberTheory.NumberField.Basic
Imported by4

Declarations

theorem

numberField_small

L27 ↗
ClassFieldTheory.numberField_small
Documentation

Every number field can be represented by a type in universe zero.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u
Lean source · statement
theorem numberField_small (F : Type u) [Field F] [NumberField F] :
    Small.{0} F
theorem

numberField_shrink

L33 ↗
ClassFieldTheory.numberField_shrink
Documentation

The shrunk model of a number field remains a number field.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ClassFieldTheory
universe u
Lean source · full declaration
theorem numberField_shrink (F : Type u) [Field F] [NumberField F] :
    letI : Small.{0} F := numberField_small F
    NumberField (Shrink.{0} F) := by
  let : Small.{0} F := numberField_small F
  exact NumberField.of_ringEquiv F (Shrink.{0} F) (Shrink.ringEquiv F).symm

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.