Module

FinitelyGeneratedCharZero.lean

Nyll.GaloisCohomology.FieldTheory.FinitelyGeneratedCharZero

4 declarations indexed from sourceView source ↗

Module documentation

Roots of unity in finitely generated fields of characteristic zero

Imports4

Nyll.GaloisCohomology.FieldTheory.FiniteAlgebraicConstants
Nyll.GaloisCohomology.FieldTheory.IntegralClosureTorsion
Mathlib.NumberTheory.NumberField.Units.Basic
Mathlib.FieldTheory.PrimeField

Imported by2

theorem

essFiniteType_rat_of_fg

L21 ↗

FieldTheory.essFiniteType_rat_of_fg

Documentation

Finitely generated fields of characteristic zero are finitely generated extensions of the rational numbers.

Source context 2 commands

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

namespace FieldTheory
universe u v

Lean source · statement

theorem essFiniteType_rat_of_fg
    (K : Type u) [Field K] [CharZero K] (hfg : Field.FG K) :
    Algebra.EssFiniteType ℚ K

theorem

finite_torsion_units_numberField

L39 ↗

FieldTheory.finite_torsion_units_numberField

Documentation

The roots of unity of a number field are exactly the torsion units of its ring of integers, hence form a finite group.

Source context 2 commands

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

namespace FieldTheory
universe u v

Lean source · statement

theorem finite_torsion_units_numberField
    (K : Type u) [Field K] [NumberField K] : Finite (CommGroup.torsion Kˣ)

theorem

finite_torsion_units_of_essFiniteType_rat

L48 ↗

FieldTheory.finite_torsion_units_of_essFiniteType_rat

Documentation

All roots of unity in a finitely generated extension of the rational numbers lie in its number field of algebraic constants.

Source context 2 commands

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

namespace FieldTheory
universe u v

Lean source · statement

theorem finite_torsion_units_of_essFiniteType_rat
    (K : Type u) [Field K] [CharZero K] [Algebra.EssFiniteType ℚ K] :
    Finite (CommGroup.torsion Kˣ)

theorem

finite_primaryComponent_finiteExtension_of_fg_charZero

L62 ↗

FieldTheory.finite_primaryComponent_finiteExtension_of_fg_charZero

Documentation

Every finite extension of a finitely generated characteristic-zero field has finite prime-primary roots of unity.

Source context 2 commands

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

namespace FieldTheory
universe u v

Lean source · statement

theorem finite_primaryComponent_finiteExtension_of_fg_charZero
    (K : Type u) [Field K] [CharZero K] (hfg : Field.FG K)
    (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L]
    (p : ℕ) [Fact p.Prime] : Finite (CommGroup.primaryComponent Lˣ p)

Module documentation

Roots of unity in finitely generated fields of characteristic zero

Declarations

essFiniteType_rat_of_fg

finite_torsion_units_numberField

finite_torsion_units_of_essFiniteType_rat

finite_primaryComponent_finiteExtension_of_fg_charZero