`Definitions/Def_Mathlib_FieldTheory_RatFuncImperfectionDegree.lean`

definition module

Degree of $K (X)$ over $K (X^{n})$ and over $K (X)^{ℓ}$

This module computes the degree of a rational function field over the subfield generated by a power of the variable, and identifies the image of Frobenius when the constants are perfect.

For a field K and n : \mathbb{N}, RatFunc.finrank_adjoin_X_pow states that K(X) has K-dimension n over the intermediate field K(X^n), obtained from the numerator and denominator of X^n (computed by RatFunc.num_X_pow, RatFunc.denom_X_pow, RatFunc.intDegree_X_pow). For n \neq 0, RatFunc.X_pow_ne_C says X^n is not a constant, hence X is integral over K(X^n) (RatFunc.isIntegral_adjoin_X_pow), and RatFunc.powerBasisAdjoinXPow is the resulting power basis of K(X) over K(X^n); its generator is X, its dimension is n, and its i-th basis vector is X^i.

In characteristic \ell a prime, RatFunc.intDegree_pow and RatFunc.pow_ne_X (for n \ge 2) give that X is not an \ell-th power, so the field range of frobenius (RatFunc K) ℓ is a proper subfield. If moreover K is perfect (a PerfectRing K ℓ instance), RatFunc.mem_fieldRange_frobenius_iff and RatFunc.fieldRange_frobenius_eq_toSubfield_adjoin identify K(X)^\ell with K(X^\ell), whence RatFunc.finrank_fieldRange_frobenius: [K(X) : K(X)^\ell] = \ell.

Transport results accompany this: Subfield.finrank_map_ringEquiv and map_fieldRange_frobenius show that a ring isomorphism carries the Frobenius subfield to the Frobenius subfield and preserves the degree (finrank_fieldRange_frobenius_eq_of_ringEquiv), while finrank_fieldRange_frobenius_eq_of_finiteDimensional proves [F:F^\ell] = [K:K^\ell] for F/K finite of characteristic \ell, by a multiplicativity argument for Subfield.relfinrank applied to the chain K^\ell \subseteq K \cap F^\ell inside F; finrank_fieldRange_frobenius_eq_of_isSeparable is the same statement with a separability instance added. Finally, for an algebra endomorphism \varphi of F with \varphi(x) = x^\ell for all x, AlgHom.finrank_fieldRange_of_forall_pow and its two corollaries give [F : \varphi(F)] = \ell when F is finite over a field isomorphic to a rational function field over a perfect field of characteristic \ell. Small helper bridges relate IntermediateField and Subfield degrees, the field range of algebraMap, and membership of aeval values in a simple adjunction; the closing statements instantiate the computation at K = \mathbb{F}_2, \ell = 2.

Relation to Mathlib

All declarations live in Mathlib namespaces and build on Mathlib's theory of RatFunc (finrank_eq_max_natDegree, adjoin_X, IntermediateField.adjoinXEquiv), PerfectRing, and Subfield.relfinrank; nothing new is defined beyond the power basis RatFunc.powerBasisAdjoinXPow and the added lemmas.

Where it is used

The imperfection degree computation is used where an endomorphism acting as x \mapsto x^\ell on a field finite over a rational function field in characteristic \ell must be shown to have image of index exactly \ell, supplying a rank input to a finiteness verification elsewhere in the development.

References

S. Lang, Algebra, 3rd revised edition, Graduate Texts in Mathematics 211, Springer, 2002, Ch. V, VII
O. Zariski and P. Samuel, Commutative Algebra II, Van Nostrand, 1960

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

390 lines
32 declarations
used in the statements of 0 theorems and imported by 1 proofs
imports 0 definition modules

Source file: Definitions/Def_Mathlib_FieldTheory_RatFuncImperfectionDegree.lean

Declarations

theoremIntermediateField.finrank_toSubfield_eq
theoremIntermediateField.aeval_mem_adjoin_singleton
theoremfinrank_fieldRange_algebraMap
theoremSubfield.finrank_map_ringEquiv
theoremmap_fieldRange_frobenius
theoremfinrank_fieldRange_frobenius_eq_of_ringEquiv
theoremfinrank_fieldRange_frobenius_eq_of_finiteDimensional
theoremfinrank_fieldRange_frobenius_eq_of_isSeparable
theoremRatFunc.num_X_pow
theoremRatFunc.denom_X_pow
theoremRatFunc.intDegree_X_pow
theoremRatFunc.X_pow_ne_C
theoremRatFunc.finrank_adjoin_X_pow
theoremRatFunc.isIntegral_adjoin_X_pow
defRatFunc.powerBasisAdjoinXPow
theoremRatFunc.powerBasisAdjoinXPow_gen
theoremRatFunc.powerBasisAdjoinXPow_dim
theoremRatFunc.powerBasisAdjoinXPow_basis_apply
theoremRatFunc.intDegree_pow
theoremRatFunc.pow_ne_X
theoremRatFunc.X_notMem_fieldRange_frobenius
theoremRatFunc.fieldRange_frobenius_ne_top
theoremRatFunc.pow_char_aeval_X
theoremRatFunc.mem_fieldRange_frobenius_iff
theoremRatFunc.fieldRange_frobenius_eq_toSubfield_adjoin
theoremRatFunc.finrank_fieldRange_frobenius
theoremAlgHom.finrank_fieldRange_of_forall_pow
theoremAlgHom.finrank_fieldRange_eq_char_of_ringEquiv_ratFunc
theoremAlgHom.finrank_fieldRange_eq_char_of_finiteDimensional
theoremRatFunc.finrank_fieldRange_frobenius_two
theoremRatFunc.gate_finrank_ne_one
theoremRatFunc.gate_engine_self

Source

import Mathlib

set_option autoImplicit false

noncomputable section

open Polynomial

section Bridges

variable {K L : Type*} [Field K] [Field L] [Algebra K L]

theorem IntermediateField.finrank_toSubfield_eq (E : IntermediateField K L) :
    Module.finrank E.toSubfield L = Module.finrank E L :=
  Algebra.finrank_eq_of_equiv_equiv
    (⟨⟨fun x => ⟨x.1, x.2⟩, fun x => ⟨x.1, x.2⟩, fun _ => rfl, fun _ => rfl⟩,
      fun _ _ => rfl, fun _ _ => rfl⟩ : E.toSubfield ≃+* E)
    (RingEquiv.refl L) (by ext x; rfl)

theorem IntermediateField.aeval_mem_adjoin_singleton (y : L) (r : Polynomial K) :
    Polynomial.aeval y r ∈ IntermediateField.adjoin K {y} :=
  IntermediateField.algebra_adjoin_le_adjoin K {y}
    (by rw [Algebra.adjoin_singleton_eq_range_aeval]; exact ⟨r, rfl⟩)

theorem finrank_fieldRange_algebraMap (K L : Type*) [Field K] [Field L] [Algebra K L] :
    Module.finrank (algebraMap K L).fieldRange L = Module.finrank K L :=
  (Algebra.finrank_eq_of_equiv_equiv (algebraMap K L).rangeRestrictFieldEquiv
    (RingEquiv.refl L) (by ext x; rfl)).symm

end Bridges

section Transport

theorem Subfield.finrank_map_ringEquiv {F F' : Type*} [Field F] [Field F'] (A : Subfield F)
    (e : F ≃+* F') :
    Module.finrank (A.map (e : F →+* F')) F' = Module.finrank A F := by
  have htop : (⊤ : Subfield F).map (e : F →+* F') = ⊤ := by
    rw [← RingHom.fieldRange_eq_map]
    exact Subfield.ext fun x =>
      ⟨fun _ => Subfield.mem_top x, fun _ => ⟨e.symm x, e.apply_symm_apply x⟩⟩
  rw [← Subfield.relfinrank_top_right (A.map (e : F →+* F')), ← htop,
    Subfield.relfinrank_map_map, Subfield.relfinrank_top_right]

variable {F F' : Type*} [Field F] [Field F'] (ℓ : ℕ) [Fact ℓ.Prime]

theorem map_fieldRange_frobenius [CharP F ℓ] [CharP F' ℓ] (e : F ≃+* F') :
    ((frobenius F ℓ).fieldRange).map (e : F →+* F') = (frobenius F' ℓ).fieldRange := by
  ext y
  simp only [Subfield.mem_map, RingHom.mem_fieldRange, frobenius_def]
  constructor
  · rintro ⟨x, ⟨g, rfl⟩, rfl⟩
    exact ⟨e g, (map_pow e g ℓ).symm⟩
  · rintro ⟨g, rfl⟩
    refine ⟨e.symm g ^ ℓ, ⟨e.symm g, rfl⟩, ?_⟩
    have h : (e : F →+* F') (e.symm g) = g := e.apply_symm_apply g
    rw [map_pow, h]

theorem finrank_fieldRange_frobenius_eq_of_ringEquiv [CharP F ℓ] [CharP F' ℓ] (e : F ≃+* F') :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius F' ℓ).fieldRange F' := by
  rw [← map_fieldRange_frobenius ℓ e, Subfield.finrank_map_ringEquiv]

end Transport

section Engine

variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ] [CharP F ℓ]

theorem finrank_fieldRange_frobenius_eq_of_finiteDimensional [FiniteDimensional K F] :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius K ℓ).fieldRange K := by

  set i : K →+* F := algebraMap K F with hi

  set KF : Subfield F := i.fieldRange with hKF

  set Kp : Subfield F := KF.map (frobenius F ℓ) with hKp

  have hcomm : (frobenius F ℓ).comp i = i.comp (frobenius K ℓ) := by
    ext x
    simp only [RingHom.comp_apply, frobenius_def, map_pow]

  have hKpKF : Kp ≤ KF := by
    rintro y hy
    rw [hKp, Subfield.mem_map] at hy
    obtain ⟨z, hz, rfl⟩ := hy
    rw [hKF, RingHom.mem_fieldRange] at hz ⊢
    obtain ⟨x, rfl⟩ := hz
    exact ⟨x ^ ℓ, by rw [map_pow]; rfl⟩
  have hKpFp : Kp ≤ (frobenius F ℓ).fieldRange := by
    rintro y hy
    rw [hKp, Subfield.mem_map] at hy
    obtain ⟨z, _, rfl⟩ := hy
    exact ⟨z, rfl⟩

  have T1 := Subfield.relfinrank_mul_finrank_top hKpKF
  have T2 := Subfield.relfinrank_mul_finrank_top hKpFp

  have S3 : Subfield.relfinrank Kp (frobenius F ℓ).fieldRange = Module.finrank KF F := by
    rw [hKp, RingHom.fieldRange_eq_map (frobenius F ℓ), Subfield.relfinrank_map_map,
      Subfield.relfinrank_top_right]

  have hKp' : Kp = ((frobenius K ℓ).fieldRange).map i := by
    rw [hKp, hKF, RingHom.fieldRange_eq_map i, Subfield.map_map, hcomm, ← Subfield.map_map,
      ← RingHom.fieldRange_eq_map]
  have hKF' : KF = (⊤ : Subfield K).map i := by
    rw [hKF, RingHom.fieldRange_eq_map]
  have S4 : Subfield.relfinrank Kp KF = Module.finrank (frobenius K ℓ).fieldRange K := by
    rw [hKp', hKF', Subfield.relfinrank_map_map, Subfield.relfinrank_top_right]

  have S5 : Module.finrank KF F = Module.finrank K F := by
    rw [hKF, hi]
    exact finrank_fieldRange_algebraMap K F
  have hpos : 0 < Module.finrank KF F := by
    rw [S5]
    exact Module.finrank_pos

  have h1 := T1.trans T2.symm
  rw [S3, S4] at h1

  rw [mul_comm (Module.finrank (frobenius K ℓ).fieldRange K)] at h1
  exact (Nat.eq_of_mul_eq_mul_left hpos h1).symm

theorem finrank_fieldRange_frobenius_eq_of_isSeparable [FiniteDimensional K F]
    [Algebra.IsSeparable K F] :
    Module.finrank (frobenius F ℓ).fieldRange F
      = Module.finrank (frobenius K ℓ).fieldRange K :=
  finrank_fieldRange_frobenius_eq_of_finiteDimensional K F ℓ

end Engine

namespace RatFunc

section AnyField

variable (K : Type*) [Field K]

@[simp]
theorem num_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).num = Polynomial.X ^ n := by
  rw [← RatFunc.algebraMap_X, ← map_pow, RatFunc.num_algebraMap]

@[simp]
theorem denom_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).denom = 1 := by
  rw [← RatFunc.algebraMap_X, ← map_pow, RatFunc.denom_algebraMap]

@[simp]
theorem intDegree_X_pow (n : ℕ) : (RatFunc.X ^ n : RatFunc K).intDegree = n := by
  rw [← RatFunc.algebraMap_X, ← map_pow, RatFunc.intDegree_polynomial,
    Polynomial.natDegree_X_pow]

theorem X_pow_ne_C {n : ℕ} (hn : n ≠ 0) (c : K) : (RatFunc.X ^ n : RatFunc K) ≠ RatFunc.C c := by
  intro h
  have hd := congrArg RatFunc.intDegree h
  rw [intDegree_X_pow, RatFunc.intDegree_C] at hd
  exact hn (by exact_mod_cast hd)

theorem finrank_adjoin_X_pow (n : ℕ) :
    Module.finrank (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)}) (RatFunc K)
      = n := by
  rw [RatFunc.finrank_eq_max_natDegree (RatFunc.X ^ n : RatFunc K), num_X_pow, denom_X_pow,
    Polynomial.natDegree_X_pow, Polynomial.natDegree_one]
  exact Nat.max_eq_left (Nat.zero_le n)

theorem isIntegral_adjoin_X_pow (n : ℕ) (hn : n ≠ 0) :
    IsIntegral (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)})
      (RatFunc.X : RatFunc K) :=
  (RatFunc.isAlgebraic_adjoin_simple_X (RatFunc.X ^ n)
    (fun ⟨c, hc⟩ => X_pow_ne_C K hn c hc)).isIntegral

noncomputable def powerBasisAdjoinXPow (n : ℕ) (hn : n ≠ 0) :
    PowerBasis (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)}) (RatFunc K) :=
  (IntermediateField.adjoin.powerBasis (isIntegral_adjoin_X_pow K n hn)).map
    (RatFunc.IntermediateField.adjoinXEquiv
      (IntermediateField.adjoin K {(RatFunc.X ^ n : RatFunc K)}))

@[simp]
theorem powerBasisAdjoinXPow_gen (n : ℕ) (hn : n ≠ 0) :
    (powerBasisAdjoinXPow K n hn).gen = RatFunc.X := by
  simp only [powerBasisAdjoinXPow, PowerBasis.map_gen,
    IntermediateField.adjoin.powerBasis_gen]
  rfl

@[simp]
theorem powerBasisAdjoinXPow_dim (n : ℕ) (hn : n ≠ 0) :
    (powerBasisAdjoinXPow K n hn).dim = n := by
  rw [← (powerBasisAdjoinXPow K n hn).finrank, finrank_adjoin_X_pow K n]

theorem powerBasisAdjoinXPow_basis_apply (n : ℕ) (hn : n ≠ 0)
    (i : Fin (powerBasisAdjoinXPow K n hn).dim) :
    (powerBasisAdjoinXPow K n hn).basis i = (RatFunc.X : RatFunc K) ^ (i : ℕ) := by
  rw [(powerBasisAdjoinXPow K n hn).basis_eq_pow i, powerBasisAdjoinXPow_gen]

end AnyField

section NotAPower

variable (K : Type*) [Field K]

theorem intDegree_pow (x : RatFunc K) (hx : x ≠ 0) (n : ℕ) :
    (x ^ n).intDegree = n * x.intDegree := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [pow_succ, RatFunc.intDegree_mul (pow_ne_zero m hx) hx, ih]
    push_cast
    ring

theorem pow_ne_X {n : ℕ} (hn : 2 ≤ n) (g : RatFunc K) : g ^ n ≠ RatFunc.X := by
  intro h
  rcases eq_or_ne g 0 with rfl | hg
  · rw [zero_pow (by omega : n ≠ 0)] at h
    exact RatFunc.X_ne_zero h.symm
  · have hd := congrArg RatFunc.intDegree h
    rw [intDegree_pow K g hg n, RatFunc.intDegree_X] at hd
    have hdvd : (n : ℤ) ∣ 1 := ⟨g.intDegree, hd.symm⟩
    have hle := Int.le_of_dvd one_pos hdvd
    omega

variable (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]

theorem X_notMem_fieldRange_frobenius :
    (RatFunc.X : RatFunc K) ∉ (frobenius (RatFunc K) ℓ).fieldRange := by
  intro hmem
  obtain ⟨g, hg⟩ := RingHom.mem_fieldRange.mp hmem
  exact pow_ne_X K (Fact.out : ℓ.Prime).two_le g hg

theorem fieldRange_frobenius_ne_top :
    (frobenius (RatFunc K) ℓ).fieldRange ≠ ⊤ := by
  intro h
  exact X_notMem_fieldRange_frobenius K ℓ (h ▸ Subfield.mem_top (RatFunc.X : RatFunc K))

end NotAPower

section PerfectConstants

variable (K : Type*) [Field K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K ℓ]

theorem pow_char_aeval_X (r : Polynomial K) :
    (Polynomial.aeval (RatFunc.X : RatFunc K) r) ^ ℓ
      = Polynomial.aeval ((RatFunc.X ^ ℓ : RatFunc K)) (r.map (frobenius K ℓ)) := by
  rw [← map_pow, ← Polynomial.map_frobenius_expand (p := ℓ) r, Polynomial.map_expand,
    Polynomial.expand_aeval]

variable [PerfectRing K ℓ]

theorem mem_fieldRange_frobenius_iff (z : RatFunc K) :
    z ∈ (frobenius (RatFunc K) ℓ).fieldRange
      ↔ z ∈ IntermediateField.adjoin K {(RatFunc.X ^ ℓ : RatFunc K)} := by
  constructor
  ·
    intro hz
    obtain ⟨g, rfl⟩ := RingHom.mem_fieldRange.mp hz
    have hg : g ∈ IntermediateField.adjoin K {(RatFunc.X : RatFunc K)} := by
      rw [RatFunc.adjoin_X]
      exact IntermediateField.mem_top
    obtain ⟨r, s, rfl⟩ := (IntermediateField.mem_adjoin_simple_iff K g).mp hg
    rw [frobenius_def, div_pow, pow_char_aeval_X K ℓ r, pow_char_aeval_X K ℓ s]
    exact div_mem (IntermediateField.aeval_mem_adjoin_singleton _ _)
      (IntermediateField.aeval_mem_adjoin_singleton _ _)
  ·
    intro hz
    obtain ⟨r, s, rfl⟩ := (IntermediateField.mem_adjoin_simple_iff K z).mp hz
    have key : ∀ t : Polynomial K,
        Polynomial.aeval ((RatFunc.X ^ ℓ : RatFunc K)) t
          ∈ (frobenius (RatFunc K) ℓ).fieldRange := by
      intro t

      have hcomp : (frobenius K ℓ).comp ((frobeniusEquiv K ℓ).symm : K →+* K)
          = RingHom.id K := by
        ext x
        exact (frobeniusEquiv K ℓ).apply_symm_apply x
      have ht : (t.map ((frobeniusEquiv K ℓ).symm : K →+* K)).map (frobenius K ℓ) = t := by
        rw [Polynomial.map_map, hcomp, Polynomial.map_id]
      rw [RingHom.mem_fieldRange]
      refine ⟨Polynomial.aeval (RatFunc.X : RatFunc K)
        (t.map ((frobeniusEquiv K ℓ).symm : K →+* K)), ?_⟩
      rw [frobenius_def, pow_char_aeval_X K ℓ, ht]
    exact div_mem (key r) (key s)

theorem fieldRange_frobenius_eq_toSubfield_adjoin :
    (frobenius (RatFunc K) ℓ).fieldRange
      = (IntermediateField.adjoin K {(RatFunc.X ^ ℓ : RatFunc K)}).toSubfield := by
  ext z
  rw [IntermediateField.mem_toSubfield]
  exact mem_fieldRange_frobenius_iff K ℓ z

theorem finrank_fieldRange_frobenius :
    Module.finrank (frobenius (RatFunc K) ℓ).fieldRange (RatFunc K) = ℓ := by
  rw [fieldRange_frobenius_eq_toSubfield_adjoin K ℓ, IntermediateField.finrank_toSubfield_eq,
    finrank_adjoin_X_pow K ℓ]

end PerfectConstants

end RatFunc

section Consumer

variable {K₀ F : Type*} [Field K₀] [Field F] [Algebra K₀ F]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ]

theorem AlgHom.finrank_fieldRange_of_forall_pow (φ : F →ₐ[K₀] F) (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = Module.finrank (frobenius F ℓ).fieldRange F := by
  have h1 : (φ : F →+* F) = frobenius F ℓ := RingHom.ext fun x => hφ x
  rw [← IntermediateField.finrank_toSubfield_eq φ.fieldRange,
    AlgHom.fieldRange_toSubfield, h1]

theorem AlgHom.finrank_fieldRange_eq_char_of_ringEquiv_ratFunc {K : Type*} [Field K]
    [CharP K ℓ] [PerfectRing K ℓ] (e : F ≃+* RatFunc K) (φ : F →ₐ[K₀] F)
    (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = ℓ := by
  rw [AlgHom.finrank_fieldRange_of_forall_pow φ hφ,
    finrank_fieldRange_frobenius_eq_of_ringEquiv ℓ e]
  exact RatFunc.finrank_fieldRange_frobenius K ℓ

theorem AlgHom.finrank_fieldRange_eq_char_of_finiteDimensional {K F₀ : Type*} [Field K]
    [Field F₀] [Algebra F₀ F] [FiniteDimensional F₀ F] [CharP K ℓ] [CharP F₀ ℓ]
    [PerfectRing K ℓ] (e : F₀ ≃+* RatFunc K) (φ : F →ₐ[K₀] F) (hφ : ∀ x, φ x = x ^ ℓ) :
    Module.finrank φ.fieldRange F = ℓ := by
  rw [AlgHom.finrank_fieldRange_of_forall_pow φ hφ,
    finrank_fieldRange_frobenius_eq_of_finiteDimensional F₀ F ℓ,
    finrank_fieldRange_frobenius_eq_of_ringEquiv ℓ e]
  exact RatFunc.finrank_fieldRange_frobenius K ℓ

end Consumer

section Gates

theorem RatFunc.finrank_fieldRange_frobenius_two :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) = 2 :=
  RatFunc.finrank_fieldRange_frobenius (ZMod 2) 2

theorem RatFunc.gate_finrank_ne_one :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) ≠ 1 := by
  rw [RatFunc.finrank_fieldRange_frobenius_two]
  omega

theorem RatFunc.gate_engine_self :
    Module.finrank (frobenius (RatFunc (ZMod 2)) 2).fieldRange (RatFunc (ZMod 2)) = 2 :=
  (finrank_fieldRange_frobenius_eq_of_finiteDimensional (RatFunc (ZMod 2))
    (RatFunc (ZMod 2)) 2).trans (RatFunc.finrank_fieldRange_frobenius (ZMod 2) 2)

end Gates

end

#print axioms IntermediateField.finrank_toSubfield_eq
#print axioms finrank_fieldRange_algebraMap
#print axioms Subfield.finrank_map_ringEquiv
#print axioms map_fieldRange_frobenius
#print axioms finrank_fieldRange_frobenius_eq_of_ringEquiv
#print axioms RatFunc.powerBasisAdjoinXPow
#print axioms RatFunc.powerBasisAdjoinXPow_gen
#print axioms RatFunc.powerBasisAdjoinXPow_dim
#print axioms RatFunc.powerBasisAdjoinXPow_basis_apply
#print axioms RatFunc.pow_ne_X
#print axioms RatFunc.X_notMem_fieldRange_frobenius
#print axioms RatFunc.fieldRange_frobenius_ne_top
#print axioms RatFunc.pow_char_aeval_X
#print axioms RatFunc.mem_fieldRange_frobenius_iff
#print axioms RatFunc.fieldRange_frobenius_eq_toSubfield_adjoin
#print axioms AlgHom.finrank_fieldRange_of_forall_pow
#print axioms AlgHom.finrank_fieldRange_eq_char_of_ringEquiv_ratFunc
#print axioms RatFunc.finrank_fieldRange_frobenius_two
#print axioms RatFunc.gate_finrank_ne_one
#print axioms RatFunc.gate_engine_self

/-- info: 'RatFunc.finrank_adjoin_X_pow' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms RatFunc.finrank_adjoin_X_pow

/-- info: 'RatFunc.finrank_fieldRange_frobenius' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms RatFunc.finrank_fieldRange_frobenius

/-- info: 'finrank_fieldRange_frobenius_eq_of_finiteDimensional' depends on axioms:
[propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms finrank_fieldRange_frobenius_eq_of_finiteDimensional

/-- info: 'finrank_fieldRange_frobenius_eq_of_isSeparable' depends on axioms:
[propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms finrank_fieldRange_frobenius_eq_of_isSeparable

/-- info: 'AlgHom.finrank_fieldRange_eq_char_of_finiteDimensional' depends on axioms:
[propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms AlgHom.finrank_fieldRange_eq_char_of_finiteDimensional

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).

Definitions/Def_Mathlib_FieldTheory_RatFuncImperfectionDegree.lean

Degree of K(X) over K(Xn) and over K(X)ℓ