NYLL
Module

KummerCover_finrank_eq.lean

Nyll.AlgebraicCurves.FunctionFields.Kummer.KummerCover_finrank_eq
2 declarations indexed from sourceView source ↗

Module documentation

Kummer Cover finrank eq

Imports1
  • Mathlib.FieldTheory.KummerExtension
Imported by1

Declarations

theorem

irreducible_X_pow_sub_C

L29 ↗
AlgebraicCurves.FunctionFields.Kummer.Proofs.KummerCover_finrank_eq.AlgebraicCurve.KummerCover.irreducible_X_pow_sub_C
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Kummer.Proofs.KummerCover_finrank_eq
open Polynomial IntermediateField
namespace AlgebraicCurve
namespace KummerCover
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem irreducible_X_pow_sub_C (hf : ∀ g : F, g ^ p ≠ f) : Irreducible (X ^ p - C f)
theorem

finrank_eq

L35 ↗
AlgebraicCurve.KummerCover.finrank_eq
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Kummer.Proofs.KummerCover_finrank_eq
open Polynomial IntermediateField
open Polynomial AlgebraicCurve.KummerCover in
Lean source · statement
theorem _root_.AlgebraicCurve.KummerCover.finrank_eq {F L : Type*} [Field F] [Field L] [Algebra F
  L] {p : ℕ} [hp : Fact p.Prime] {f : F}
    [IsSplittingField F L (X ^ p - C f)] (hζ : (primitiveRoots p F).Nonempty) (hf : ∀ g : F, g ^ p
      ≠ f) :
    Module.finrank F L = p

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