Module

Algebra_IsSeparable_of_finrank_fieldRange_frobenius_eq.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.Algebra_IsSeparable_of_finrank_fieldRange_frobenius_eq

1 declaration indexed from sourceView source ↗

Module documentation

Algebra Is Separable of finrank field Range frobenius eq

Imports7

Mathlib.RingTheory.Unramified.Field
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.Algebra.CharP.Frobenius
Mathlib.Algebra.Field.Subfield.Basic
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.FieldTheory.Separable

Imported by3

theorem

of_finrank_fieldRange_frobenius_eq

L29 ↗

Algebra.IsSeparable.of_finrank_fieldRange_frobenius_eq

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs.AlgebraIsSeparableFinrankField

Lean source · statement

theorem _root_.Algebra.IsSeparable.of_finrank_fieldRange_frobenius_eq
    {E F : Type*} [Field E] [Field F] [Algebra E F] [FiniteDimensional E F]
    (p : ℕ) [Fact p.Prime] [CharP F p]
    (hdeg : Module.finrank (frobenius F p).fieldRange F = p)
    (y : E) (hy : algebraMap E F y ∉ (frobenius F p).fieldRange) :
    Algebra.IsSeparable E F

Module documentation

Algebra Is Separable of finrank field Range frobenius eq

Declarations

of_finrank_fieldRange_frobenius_eq