unramified extensions of local fields

Stream: Is there code for X?

[Kevin Buzzard]

After several years and a lot of frustration, we now have docs#IsNonarchimedeanLocalField , a way of saying "let K be a nonarchimedean local field".

I think the next key construction needed for local class field theory is to be able to talk about unramified extensions in this context. I have tried to map out a suggestion of how this might look in mathlib, although I would welcome other ideas.

1) IsUnramified. This is a predicate on field extensions which should probably exist in more generality than the nonarch local case. My impression is that @Adam Topaz knows how we should be stating this, and in what generality the predicate should exist. Whatever the main result about this predicate is, it should imply that if L/K is a finite Galois unramified extension of nonarch local fields, then there's a "functorial" isomorphism Gal(L/K)=Gal(l/k) with l,k the residue fields. It might be a construction which gives a bijection between the K-algebra maps L->M of unramified extensions, and the k-algebra maps l->m? This is probably not about local fields at all, but the fact that we now have docs#ValuativeRel probably means that we're ready to tackle this in the correct generality.

2) UnramifiedLift. Again here I'm not entirely clear about the generality, but if K is in some class of fields which include nonarch local fields, with residue field k, and if l/k is a separable(?) extension then we want a construction which gives the corresponding unramified extension of K. In my mind this is $K\otimes_{W(k)}W(l)$, which opens up a whole new can of worms which I'll deal with next; are there other (better?) ways to do this?

3) API for Witt vectors. If $R$ is an Artin local ring with residue field $k$ of characteristic $p$ then $R$ is uniquely a $W(k)$-algebra. Does this sound right? Do we have it? I'm making this up as I go along based only on my vibes-based understnading of Witt vectors. If $R$ is a complete Noetherian local ring with the maximal-ideal-adic topology and residue field $k$ of char $p$ then I claim there's a unique ring map $W(k)\to R$ and if $W(k)$ has the $p$-adic topology then this map is continuous. I even claim that if $R$ is a compact Hausdorff topological ring with open maximal ideal (and thus finite residue field $k$) then $R$ is canonically a $W(k)$-algebra and the structure map is continuous; no Noetherian hypotheses needed. This might be hard (I think it uses that compact Hausdorff commutative topological rings are profinite, a fact which Andrew Yang pointed out to me and which surprised me). We'll need things like: base change of unramified is unramified, Frac(W(l))/Frac(W(k)) is unramified etc.

4) Galois theory of finite fields. Do we have that if $k$ is finite and $n\in\Z_{\geq1}$ then there's a unique (up to in general non-unique isomorphism) extension of $k$ of degree $n$, and this extension is finite and Galois with Galois group cyclic of degree $n$, and arithmetic Frobenius is a generator?

---

One of the statements I need for local class field theory is "if $K$ is nonarch local and if $n$ is a positive natural then there's a unique unramified extension $L/K$ of degree $n$, which is Galois, and the canonical map $Gal(L/K)\to Gal(l/k)$ is a group iso. I would like to pass this project onto the class field theory project but this stuff is sufficiently close to the boundary of mathlib that I feel like it should be done in the correct generality and PRed directly to mathlib rather than to the CFT repo. We can perhaps use the CFT repo as a staging ground for it but I would like to be clear on the approach which the experts think is mathlib-worthy before I launch into anything.

[Kenny Lau]

@Kevin Buzzard for 4 (finite fields) I think Mathlib.FieldTheory.Finite.GaloisField should have everything you need (at least the basic ingredients, you might need to assemble them yourself)

[Andrew Yang]

1) According to #maths > what is an unramified extension? the consensus seems to be that a unramified extension of fields with valative rels is one where the map on valuative group is surjective (and hence bijective).

[Adam Topaz]

For an extension of valued fields $(L,w) | (K,v)$, the usual way to say that this extension is unramified is by saying that the ramification degree (i.e. the index $[\Gamma_w : \Gamma_v]$) is $1$, and that the residue extension is separable. The condition about the residue extension can be stated in terms of docs#Algebra.IsSeparable and the condition about the ramification degree is equivalent to:

import Mathlib

class IsPreUnramified
    {K L : Type*}
    [Field K] [Field L]
    [ValuativeRel K] [ValuativeRel L]
    [Algebra K L] [ValuativeExtension K L] : Prop where
  isPreUnramified : ∀ l : L, ∃ (k : K) (u : L),
      ValuativeRel.valuation _ u = 1 ∧ l = algebraMap _ _ k * u

[Adam Topaz]

Of course for local fields the residue field condition is automatic, but in general it's not.

[Adam Topaz]

It would be great to come up with some condition that's easy to work with in terms of ValuativeRel, and which we can show is related to docs#RingHom.Etale

[Riccardo Brasca]

We already have Algebra.IsUnramifiedAt that is completely general, and Algebra.isUnramifiedAt_iff_map_eq to connect it with the usual number theoretical condition

[Adam Topaz]

That would work too.

[Andrew Yang]

Algebra.IsUnramifiedAt is only well-behaved for finite extensions though. Does this def for valuative rel work for infinite extensions?

[Riccardo Brasca]

@Kevin Buzzard the existence and unicity of an unramified extension is I think completely doable.

[Adam Topaz]

Andrew Yang said:

Algebra.IsUnramifiedAt is only well-behaved for finite extensions though. Does this def for valuative rel work for infinite extensions?

yes, and that's a good point.

[Riccardo Brasca]

For the existence we have Dedekind criterion, so one can just take the minimal polynomial of a generator of the residual extension and lift it

[Adam Topaz]

The statement about the correspondence between unramified extensions and extensions of the residue fields should work in full generality as long as the residue field of the base is perfect.

[Adam Topaz]

(It's also possible to relax this condition about being perfect to some extent IIRC)

[Adam Topaz]

I think pretty much all this general valuation theory can be found in Commutative algebra II by Zariski-Samuel

[Adam Topaz]

... but it seems I don't have online access from my uni's library atm :-/

[Aaron Liu]

For 4) I see

• finite fields of the same cardinality are ring equiv (docs#FiniteField.ringEquivOfCardEq)
• finite fields of cardinality p^n exist (docs#GaloisField)
• extensions of finite fields are galois (docs#GaloisField.instIsGaloisOfFinite)
• galois group of extension of finite fields is exactly the powers of arithmetic frobenius (docs#FiniteField.bijective_frobeniusAlgHom_pow)
• extensions of finite fields are finite (docs#Module.Finite.of_finite)
• cardinality of finite field is a power of the characteristic (docs#FiniteField.card)

I can't seem to find "there exists a degree n extension of any finite field"

[Kenny Lau]

@Kevin Buzzard for 4 i've tried to put the pieces together but there are still 3 sorries left:

import Mathlib.FieldTheory.Finite.GaloisField

/- Galois theory of finite fields. Do we have that if $$k$$ is finite and $$n\in\Z_{\geq1}$$ then
there's a unique (up to in general non-unique isomorphism) extension of $$k$$ of degree $$n$$, and
this extension is finite and Galois with Galois group cyclic of degree $$n$$, and arithmetic
Frobenius is a generator?
-/

variable (k : Type*) [Field k] [Finite k]
variable (p : ℕ) [Fact p.Prime] [Algebra (ZMod p) k]
variable (n : ℕ) [NeZero n]

open Polynomial

/-! # exists l/k deg n -/

#check Module.finrank (ZMod p) k -- this is m such that [k:Fp] = m

/-- Non-canoncailly chosen extension -/
noncomputable def FiniteFieldExtension : Type :=
  GaloisField p (Module.finrank (ZMod p) k * n)

noncomputable instance : Field (FiniteFieldExtension k p n) :=
  instFieldGaloisField _ _

noncomputable instance : Finite (FiniteFieldExtension k p n) :=
  instFiniteGaloisField _ _

noncomputable instance : Algebra (ZMod p) (FiniteFieldExtension k p n) :=
  instAlgebraZModGaloisField _ _

theorem nonempty_algHom_finiteFieldExtension :
    Nonempty (k →ₐ[ZMod p] FiniteFieldExtension k p n) := by
  have := Fintype.ofFinite k
  have := FiniteField.isSplittingField_sub k (ZMod p)
  exact ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card k - X) sorry⟩

noncomputable instance : Algebra k (FiniteFieldExtension k p n) :=
  (nonempty_algHom_finiteFieldExtension k p n).some.toAlgebra

instance : IsScalarTower (ZMod p) k (FiniteFieldExtension k p n) :=
  -- there is only at most one map from Fp to any ring
  .of_algebraMap_eq' <| Subsingleton.elim _ _

theorem natCard_finiteFieldExtension : Nat.card (FiniteFieldExtension k p n) = Nat.card k ^ n := by
  rw [FiniteFieldExtension, GaloisField.card, pow_mul]
  conv => enter [1,1,1]; rw [← ZMod.card p]
  rw [Fintype.card_eq_nat_card, ← Module.natCard_eq_pow_finrank]
  exact mul_ne_zero sorry (NeZero.ne n)

/-! # degree n -/

theorem finrank_finiteFieldExtension : Module.finrank k (FiniteFieldExtension k p n) = n := by
  refine Nat.pow_right_injective (sorry : 2 ≤ Nat.card k) ?_
  simp only [← Module.natCard_eq_pow_finrank, natCard_finiteFieldExtension]

/-! # extension is finite -/

theorem moduleFinite_finiteFieldExtension : Module.Finite k (FiniteFieldExtension k p n) :=
  Module.finite_of_finrank_pos <| (finrank_finiteFieldExtension k p n).symm ▸ NeZero.pos n

instance : IsSplittingField k (FiniteFieldExtension k p n) (X ^ Nat.card k ^ n - X) := by
  have := Fintype.ofFinite (FiniteFieldExtension k p n)
  convert FiniteField.isSplittingField_sub (FiniteFieldExtension k p n) k
  · rw [Fintype.card_eq_nat_card, natCard_finiteFieldExtension]

/-! # galois -/

instance : IsGalois k (FiniteFieldExtension k p n) :=
  GaloisField.instIsGaloisOfFinite

/-! # cyclic -/

instance : IsCyclic Gal(FiniteFieldExtension k p n / k) :=
  FiniteField.instIsCyclicAlgEquivOfFinite _ _

/-! # frobenius generator -/

noncomputable def FiniteFieldExtension.frob :
    FiniteFieldExtension k p n ≃ₐ[k] FiniteFieldExtension k p n :=
  haveI := Fintype.ofFinite k
  FiniteField.frobeniusAlgEquivOfAlgebraic _ _

theorem FiniteFieldExtension.frob_generates (g : Gal(FiniteFieldExtension k p n / k)) :
    ∃ i < n, FiniteFieldExtension.frob k p n ^ i = g := by
  have := Fintype.ofFinite k
  obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (FiniteFieldExtension k p n)).2 g
  refine ⟨i, ?_, by ext; simp [frob]; congr; subsingleton⟩
  rwa [finrank_finiteFieldExtension] at hi

/-! # l/k deg n is unique  -/

theorem unique_finiteFieldExtension (l : Type*) [Field l] [Algebra k l]
    (h : Module.finrank k l = n) : Nonempty (l ≃ₐ[k] FiniteFieldExtension k p n) := by
  have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n
  have : Finite l := Module.finite_of_finite k
  have : Fintype l := .ofFinite _
  have : IsSplittingField k l (X ^ Nat.card k ^ n - X) := by
    convert FiniteField.isSplittingField_sub l k
    rw [← h, ← Module.natCard_eq_pow_finrank, Fintype.card_eq_nat_card]
  refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩
  exact (IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).symm

[Kevin Buzzard]

It occurs to me that (2) might actually be a special case of some vastly more general claim about formal lifting of morphisms along locally nilpotent extensions or whatever; I don't know enough alg geom to know what the correct theorem is here -- maybe lifting etale morphisms?

[Kevin Buzzard]

@Kenny Lau For the first sorry this would help:

example (k : Type*) [Field k] (f g : k[X]) (h : f ∣ g) :
    Splits (algebraMap k g.SplittingField) f := sorry

[Kenny Lau]

Polynomial.splits_of_splits_of_dvd exists already, but i can't find the lemma that x^q-x divides x^q^n-x

[Kevin Buzzard]

This is f|g -> xf|xg and a | b implies x^a-1 | x^b-1 (and a-1 | a^n-1)

[Yakov Pechersky]

There will be some friction between using IsUnramifiedAt and having to refer to the (ValuativeRel?) O[K], linking Localization.AtPrime with the field you started with, and dealing with the concrete case of (p), Q_p, and Z_p vs Q_p and O[Q_p].

[Yakov Pechersky]

To clarify, I am not saying that one shouldn't use that API. I am just describing the various glue that is currently missing.

[Kevin Buzzard]

Progress on second sorry:

theorem natCard_finiteFieldExtension : Nat.card (FiniteFieldExtension k p n) = Nat.card k ^ n := by
  rw [FiniteFieldExtension, GaloisField.card, pow_mul]
  conv => enter [1,1,1]; rw [← ZMod.card p]
  rw [Fintype.card_eq_nat_card, ← Module.natCard_eq_pow_finrank]
  exact mul_ne_zero (by
    intro h
    unfold Module.finrank at h
    rw [Cardinal.toNat_eq_zero] at h
    obtain htrue | hnonsense := h
    · have bar : Subsingleton k := by
        apply Module.subsingleton_of_rank_zero htrue
      exact false_of_nontrivial_of_subsingleton k
    · have foo : Infinite k := by
        -- hnonsense : Cardinal.aleph0 ≤ Module.rank (ZMod p) k
        sorry
      exact _root_.not_finite k
    ) (NeZero.ne n)

Reduced to

hnonsense : Cardinal.aleph0 ≤ Module.rank (ZMod p) k
⊢ Infinite k

but the only theorems with hypothesis Cardinal.aleph0 ≤ Module.rank (ZMod p) k are useless ones about the rank of the dual.

[Kenny Lau]

there is Module.Finite.of_finite

[Kevin Buzzard]

Oh wait, it's much easier with docs#Module.finrank_eq_zero_iff

[Kevin Buzzard]

theorem Module.finrank_ne_zero
    {R : Type*} [Ring R] {M : Type*} [AddCommGroup M] [Module R M]
    [StrongRankCondition R] [Module.Finite R M] [Nontrivial M]
    [NoZeroSMulDivisors R M] : Module.finrank R M ≠ 0 := by
  intro h
  rw [Module.finrank_eq_zero_iff] at h
  obtain ⟨m, hm⟩ := exists_ne (0 : M)
  obtain ⟨a, ha, ha1⟩ := h m
  exact ha <| (smul_eq_zero_iff_left hm).mp ha1

theorem natCard_finiteFieldExtension : Nat.card (FiniteFieldExtension k p n) = Nat.card k ^ n := by
  rw [FiniteFieldExtension, GaloisField.card, pow_mul]
  conv => enter [1,1,1]; rw [← ZMod.card p]
  · rw [Fintype.card_eq_nat_card, ← Module.natCard_eq_pow_finrank]
  · exact mul_ne_zero Module.finrank_ne_zero (NeZero.ne n)

[Kevin Buzzard]

The other sorry is

theorem Nat.two_le_card {M : Type*} [Nontrivial M] [Finite M] :
    2 ≤ Nat.card M := by

(working on it)

[Bhavik Mehta]

That should be basically immediate from docs#Finite.one_lt_card

[Kevin Buzzard]

Aah, loogle was giving me nothing for 2 <= stuff, but apparently that's not how we spell it!

[Bhavik Mehta]

I searched Nat.card and Nontrivial here

[Kevin Buzzard]

My searches were not as clean because I hadn't arrived at the statement of the theorem at that point (I was doing nontrivial modules initially); I should have searched again once I realised what I was trying to prove!

[Kevin Buzzard]

lol 1 < card and 2<= card are defeq ;-)

[Bhavik Mehta]

hence "basically immediate" :-)

[Kevin Buzzard]

So is docs#Nat.pow_right_injective not stated idiomatically? (that's where Kenny got the 2 <= a goal from)

[Kenny Lau]

i think both spellings are used (at least there is also Nat.Prime.two_le)

[Kevin Buzzard]

Sorry-free:

import Mathlib.FieldTheory.Finite.GaloisField

/- Galois theory of finite fields. Do we have that if $$k$$ is finite and $$n\in\Z_{\geq1}$$ then
there's a unique (up to in general non-unique isomorphism) extension of $$k$$ of degree $$n$$, and
this extension is finite and Galois with Galois group cyclic of degree $$n$$, and arithmetic
Frobenius is a generator?
-/

variable (k : Type*) [Field k] [Finite k]
variable (p : ℕ) [Fact p.Prime] [Algebra (ZMod p) k]
variable (n : ℕ) [NeZero n]

open Polynomial

/-! # exists l/k deg n -/

/-- Non-canoncailly chosen extension -/
noncomputable def FiniteFieldExtension : Type :=
  GaloisField p (Module.finrank (ZMod p) k * n)

noncomputable instance : Field (FiniteFieldExtension k p n) :=
  instFieldGaloisField _ _

noncomputable instance : Finite (FiniteFieldExtension k p n) :=
  instFiniteGaloisField _ _

noncomputable instance : Algebra (ZMod p) (FiniteFieldExtension k p n) :=
  instAlgebraZModGaloisField _ _

-- should be elsewhere
theorem Module.finrank_ne_zero
    {R : Type*} [Ring R] {M : Type*} [AddCommGroup M] [Module R M]
    [StrongRankCondition R] [Module.Finite R M] [Nontrivial M]
    [NoZeroSMulDivisors R M] : Module.finrank R M ≠ 0 := by
  intro h
  rw [Module.finrank_eq_zero_iff] at h
  obtain ⟨m, hm⟩ := exists_ne (0 : M)
  obtain ⟨a, ha, ha1⟩ := h m
  exact ha <| (smul_eq_zero_iff_left hm).mp ha1

-- stunned that we don't have this!
theorem dvd_pow_sub_one_of_dvd {R : Type*} [CommRing R] {r : R} {a b : ℕ} (h : a ∣ b) :
    r ^ a - 1 ∣ r ^ b - 1 := by
  obtain ⟨n, rfl⟩ := h
  exact pow_one_sub_dvd_pow_mul_sub_one r a n -- we have a worse version and it's misnamed

theorem nonempty_alghom_of_finrank_dvd {p : ℕ} (hp : p.Prime)
    {k : Type*} [Field k] [Finite k] [Algebra (ZMod p) k]
    {l : Type*} [Field l] [Finite l] [Algebra (ZMod p) l]
    (h : Module.finrank (ZMod p) k ∣ Module.finrank (ZMod p) l) :
    Nonempty (k →ₐ[ZMod p] l) :=
  have := Fintype.ofFinite k
  have := Fintype.ofFinite l
  have := Fact.mk hp
  -- construct the map using properties of splitting fields
  ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card k - X) <| by
    -- need to check x^#k-x splits in l so use handy lemma from library
    refine Polynomial.splits_of_splits_of_dvd _  ?_
      (FiniteField.isSplittingField_sub l (ZMod p)).splits ?_
    -- nonzeroness needed to apply the lemma
    · rw [Fintype.card_eq_nat_card, Module.natCard_eq_pow_finrank (K := ZMod p)]
      refine FiniteField.X_pow_card_pow_sub_X_ne_zero (ZMod p) Module.finrank_ne_zero ?_
      simpa using hp.one_lt
    -- now it's algebra: x^#k-x | x^#l-x with dim k | dim l
    -- Am I making a meal of this?
    · suffices (X : (ZMod p)[X]) ^ (Fintype.card k - 1) - 1 ∣ X ^ (Fintype.card l - 1) - 1 by
        have := mul_dvd_mul_left X this
        simpa [mul_sub, ← pow_succ', Nat.sub_one_add_one (Fintype.card_ne_zero)]
      rw [Fintype.card_eq_nat_card, Module.natCard_eq_pow_finrank (K := ZMod p),
        Nat.card_eq_fintype_card, ZMod.card]
      rw [Fintype.card_eq_nat_card, Module.natCard_eq_pow_finrank (K := ZMod p),
        Nat.card_eq_fintype_card, ZMod.card]
      apply dvd_pow_sub_one_of_dvd -- first of two independent usages ;-)
      zify
      simp [Int.ofNat_sub (NeZero.one_le), dvd_pow_sub_one_of_dvd h]
  ⟩

theorem nonempty_algHom_finiteFieldExtension :
    Nonempty (k →ₐ[ZMod p] FiniteFieldExtension k p n) := by
  apply nonempty_alghom_of_finrank_dvd Fact.out
  simp [FiniteFieldExtension,
    GaloisField.finrank p (mul_ne_zero Module.finrank_ne_zero (NeZero.ne n))]

noncomputable instance : Algebra k (FiniteFieldExtension k p n) :=
  (nonempty_algHom_finiteFieldExtension k p n).some.toAlgebra

instance : IsScalarTower (ZMod p) k (FiniteFieldExtension k p n) :=
  -- there is only at most one map from Fp to any ring
  .of_algebraMap_eq' <| Subsingleton.elim _ _

theorem natCard_finiteFieldExtension : Nat.card (FiniteFieldExtension k p n) = Nat.card k ^ n := by
  rw [FiniteFieldExtension, GaloisField.card, pow_mul]
  conv => enter [1,1,1]; rw [← ZMod.card p]
  · rw [Fintype.card_eq_nat_card, ← Module.natCard_eq_pow_finrank]
  · exact mul_ne_zero Module.finrank_ne_zero (NeZero.ne n)

/-! # degree n -/

theorem finrank_finiteFieldExtension : Module.finrank k (FiniteFieldExtension k p n) = n := by
  refine Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_
  simp only [← Module.natCard_eq_pow_finrank, natCard_finiteFieldExtension]

/-! # extension is finite -/

theorem moduleFinite_finiteFieldExtension : Module.Finite k (FiniteFieldExtension k p n) :=
  Module.finite_of_finrank_pos <| (finrank_finiteFieldExtension k p n).symm ▸ NeZero.pos n

instance : IsSplittingField k (FiniteFieldExtension k p n) (X ^ Nat.card k ^ n - X) := by
  have := Fintype.ofFinite (FiniteFieldExtension k p n)
  convert FiniteField.isSplittingField_sub (FiniteFieldExtension k p n) k
  · rw [Fintype.card_eq_nat_card, natCard_finiteFieldExtension]

/-! # galois -/

instance : IsGalois k (FiniteFieldExtension k p n) :=
  GaloisField.instIsGaloisOfFinite

/-! # cyclic -/

instance : IsCyclic Gal(FiniteFieldExtension k p n / k) :=
  FiniteField.instIsCyclicAlgEquivOfFinite _ _

/-! # frobenius generator -/

noncomputable def FiniteFieldExtension.frob :
    FiniteFieldExtension k p n ≃ₐ[k] FiniteFieldExtension k p n :=
  haveI := Fintype.ofFinite k
  FiniteField.frobeniusAlgEquivOfAlgebraic _ _

theorem FiniteFieldExtension.frob_generates (g : Gal(FiniteFieldExtension k p n/k)) :
    ∃ i < n, FiniteFieldExtension.frob k p n ^ i = g := by
  have := Fintype.ofFinite k
  obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (FiniteFieldExtension k p n)).2 g
  refine ⟨i, ?_, by ext; simp [frob]; congr; subsingleton⟩
  rwa [finrank_finiteFieldExtension] at hi

/-! # l/k deg n is unique  -/

theorem unique_finiteFieldExtension (l : Type*) [Field l] [Algebra k l]
    (h : Module.finrank k l = n) : Nonempty (l ≃ₐ[k] FiniteFieldExtension k p n) := by
  have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n
  have : Finite l := Module.finite_of_finite k
  have : Fintype l := .ofFinite _
  have : IsSplittingField k l (X ^ Nat.card k ^ n - X) := by
    convert FiniteField.isSplittingField_sub l k
    rw [← h, ← Module.natCard_eq_pow_finrank, Fintype.card_eq_nat_card]
  refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩
  exact (IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).symm

[Ruben Van de Velde]

\N should be enough for anyone, right? docs#Nat.pow_sub_one_dvd_pow_sub_one

[Kenny Lau]

they are polynomials here

[Kevin Buzzard]

Well, the first one was :-) The second one was nat so probably my zify is unnecessary.

[Kevin Buzzard]

Good to see they went with pow_sub_one rather than pow_one_sub in the Nat case though.

[Ruben Van de Velde]

Eventually-

@[deprecated Nat.sub_one_dvd_pow_sub_one (since := "2025-08-23")]
theorem Nat.nat_pow_one_sub_dvd_pow_mul_sub_one

[Riccardo Brasca]

Someone should PR this!

[Ruben Van de Velde]

I was assuming @Kevin Buzzard would

[Kevin Buzzard]

I thought Kenny already did -- #30738

[Kenny Lau]

it compiles now