NYLL
Module

FinitelyGeneratedPositiveChar.lean

Nyll.GaloisCohomology.FieldTheory.FinitelyGeneratedPositiveChar
5 declarations indexed from sourceView source ↗

Module documentation

Constants in finitely generated fields of positive characteristic

Imports3
Imported by4

Declarations

theorem

finite_primeSubfield_of_ringChar_ne_zero

L19 ↗
FieldTheory.finite_primeSubfield_of_ringChar_ne_zero
Documentation

The prime subfield of a field of positive characteristic is finite.

Source context 2 commands

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

namespace FieldTheory
universe u v
Lean source · statement
theorem finite_primeSubfield_of_ringChar_ne_zero
    (K : Type u) [Field K] (hchar : ringChar K ≠ 0) :
    Finite (⊥ : Subfield K)
theorem

finite_constants_of_fg_posChar

L30 ↗
FieldTheory.finite_constants_of_fg_posChar
Documentation

The algebraic constants in a finitely generated field of positive characteristic form a finite field.

Source context 2 commands

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

namespace FieldTheory
universe u v
Lean source · statement
theorem finite_constants_of_fg_posChar
    (K : Type u) [Field K] (hfg : Field.FG K) (hchar : ringChar K ≠ 0) :
    Finite (algebraicClosure (⊥ : Subfield K) K)
theorem

finite_torsion_units_of_fg_posChar

L38 ↗
FieldTheory.finite_torsion_units_of_fg_posChar
Documentation

Every root of unity is contained in the finite 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_fg_posChar
    (K : Type u) [Field K] (hfg : Field.FG K) (hchar : ringChar K ≠ 0) :
    Finite (CommGroup.torsion Kˣ)
theorem

exists_not_artinSchreier_of_fg_posChar

L47 ↗
FieldTheory.exists_not_artinSchreier_of_fg_posChar
Documentation

The Artin--Schreier map on a finitely generated field of positive characteristic is not surjective.

Source context 2 commands

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

namespace FieldTheory
universe u v
Lean source · statement
theorem exists_not_artinSchreier_of_fg_posChar
    (K : Type u) [Field K] (hfg : Field.FG K) (hchar : ringChar K ≠ 0) :
    ∃ a : K, ∀ x : K, x ^ ringChar K - x ≠ a
theorem

finite_primaryComponent_finiteExtension_of_fg_posChar

L56 ↗
FieldTheory.finite_primaryComponent_finiteExtension_of_fg_posChar
Documentation

The primary roots of unity in every finite extension are finite.

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_posChar
    (K : Type u) [Field K] (hfg : Field.FG K) (hchar : ringChar K ≠ 0)
    (L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L]
    (p : ℕ) [Fact p.Prime] : Finite (CommGroup.primaryComponent Lˣ p)

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