[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
cases' CharP.exists α with p _
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
haveI hp := Fact.mk (CharP.char_is_prime α p)
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
letI : Algebra (ZMod p) α := ZMod.algebra _ _
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
let b := IsNoetherian.finsetBasis (ZMod p) α
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow p
[PROOFSTEP]
exact hp.1.isPrimePow
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ ‖{ x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α }‖ ≠ 0
[PROOFSTEP]
rw [← FiniteDimensional.finrank_eq_card_basis b]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ FiniteDimensional.finrank (ZMod p) α ≠ 0
[PROOFSTEP]
exact FiniteDimensional.finrank_pos.ne'
[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖
[PROOFSTEP]
refine' ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, _⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ IsPrimePow ‖α‖ → Nonempty (Field α)
[PROOFSTEP]
rintro ⟨p, n, hp, hn, hα⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Nonempty (Field α)
[PROOFSTEP]
haveI := Fact.mk hp.nat_prime
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
⊢ Nonempty (Field α)
[PROOFSTEP]
exact ⟨(Fintype.equivOfCardEq ((GaloisField.card p n hn.ne').trans hα)).symm.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
⊢ Nonempty (Field α)
[PROOFSTEP]
letI K := FractionRing (MvPolynomial α <| ULift.{u} ℚ)
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ Nonempty (Field α)
[PROOFSTEP]
suffices #α = #K by
  obtain ⟨e⟩ := Cardinal.eq.1 this
  exact ⟨e.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
this : #α = #K
⊢ Nonempty (Field α)
[PROOFSTEP]
obtain ⟨e⟩ := Cardinal.eq.1 this
[GOAL]
case intro
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
this : #α = #K
e : α ≃ K
⊢ Nonempty (Field α)
[PROOFSTEP]
exact ⟨e.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α = #K
[PROOFSTEP]
rw [← IsLocalization.card (MvPolynomial α <| ULift.{u} ℚ)⁰ K le_rfl]
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α = #(MvPolynomial α (ULift ℚ))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α ≤ #(MvPolynomial α (ULift ℚ))
[PROOFSTEP]
refine' ⟨⟨fun a => MvPolynomial.monomial (Finsupp.single a 1) (1 : ULift.{u} ℚ), fun x y h => _⟩⟩
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
x y : α
h :
  (fun a => ↑(MvPolynomial.monomial (Finsupp.single a 1)) 1) x =
    (fun a => ↑(MvPolynomial.monomial (Finsupp.single a 1)) 1) y
⊢ x = y
[PROOFSTEP]
simpa [MvPolynomial.monomial_eq_monomial_iff, Finsupp.single_eq_single_iff] using h
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #(MvPolynomial α (ULift ℚ)) ≤ #α
[PROOFSTEP]
simp
[GOAL]
α : Type u
⊢ Nonempty (Field α) ↔ IsPrimePow #α
[PROOFSTEP]
rw [Cardinal.isPrimePow_iff]
[GOAL]
α : Type u
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
cases' fintypeOrInfinite α with h h
[GOAL]
case inl
α : Type u
h : Fintype α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left', (Cardinal.nat_lt_aleph0 _).not_le, false_or_iff] using
  Fintype.nonempty_field_iff
[GOAL]
case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simpa only [← Cardinal.infinite_iff, h, true_or_iff, iff_true_iff] using Infinite.nonempty_field
