[GOAL]
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ↑(frobenius (MvPolynomial σ (ZMod p)) p) f = ↑(expand p) f
[PROOFSTEP]
apply induction_on f
[GOAL]
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), ↑(frobenius (MvPolynomial σ (ZMod p)) p) (↑C a) = ↑(expand p) (↑C a)
[PROOFSTEP]
intro a
[GOAL]
case h_C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ ↑(frobenius (MvPolynomial σ (ZMod p)) p) (↑C a) = ↑(expand p) (↑C a)
[PROOFSTEP]
rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]
[GOAL]
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 = ↑(expand p) p_1 →
      ↑(frobenius (MvPolynomial σ (ZMod p)) p) q = ↑(expand p) q →
        ↑(frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = ↑(expand p) (p_1 + q)
[PROOFSTEP]
simp only [AlgHom.map_add, RingHom.map_add]
[GOAL]
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 = ↑(expand p) p_1 →
      ↑(frobenius (MvPolynomial σ (ZMod p)) p) q = ↑(expand p) q →
        ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 + ↑(frobenius (MvPolynomial σ (ZMod p)) p) q =
          ↑(expand p) p_1 + ↑(expand p) q
[PROOFSTEP]
intro _ _ hf hg
[GOAL]
case h_add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
hf : ↑(frobenius (MvPolynomial σ (ZMod p)) p) p✝ = ↑(expand p) p✝
hg : ↑(frobenius (MvPolynomial σ (ZMod p)) p) q✝ = ↑(expand p) q✝
⊢ ↑(frobenius (MvPolynomial σ (ZMod p)) p) p✝ + ↑(frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
    ↑(expand p) p✝ + ↑(expand p) q✝
[PROOFSTEP]
rw [hf, hg]
[GOAL]
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 = ↑(expand p) p_1 →
      ↑(frobenius (MvPolynomial σ (ZMod p)) p) (p_1 * X n) = ↑(expand p) (p_1 * X n)
[PROOFSTEP]
simp only [expand_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 = ↑(expand p) p_1 →
      ↑(frobenius (MvPolynomial σ (ZMod p)) p) p_1 * ↑(frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        ↑(expand p) p_1 * X n ^ p
[PROOFSTEP]
intro _ _ hf
[GOAL]
case h_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : ↑(frobenius (MvPolynomial σ (ZMod p)) p) p✝ = ↑(expand p) p✝
⊢ ↑(frobenius (MvPolynomial σ (ZMod p)) p) p✝ * ↑(frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) =
    ↑(expand p) p✝ * X n✝ ^ p
[PROOFSTEP]
rw [hf, frobenius_def]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
⊢ ↑(eval a) (indicator a) = 1
[PROOFSTEP]
nontriviality
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
⊢ ↑(eval a) (indicator a) = 1
[PROOFSTEP]
have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
✝ : Nontrivial ((fun x => K) (indicator a))
this : 0 < Fintype.card K - 1
⊢ ↑(eval a) (indicator a) = 1
[PROOFSTEP]
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self, zero_pow this, sub_zero,
  Finset.prod_const_one]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ degrees (indicator c) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
[PROOFSTEP]
rw [indicator]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1))) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
[PROOFSTEP]
refine' le_trans (degrees_prod _ _) (Finset.sum_le_sum fun s _ => _)
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (1 - (X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
[PROOFSTEP]
refine' le_trans (degrees_sub _ _) _
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ⊔ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
[PROOFSTEP]
rw [degrees_one, ← bot_eq_zero, bot_sup_eq]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees ((X s - ↑C (c s)) ^ (Fintype.card K - 1)) ≤ (Fintype.card K - 1) • {s}
[PROOFSTEP]
refine' le_trans (degrees_pow _ _) (nsmul_le_nsmul_of_le_right _ _)
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s - ↑C (c s)) ≤ {s}
[PROOFSTEP]
refine' le_trans (degrees_sub _ _) _
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ⊔ degrees (↑C (c s)) ≤ {s}
[PROOFSTEP]
rw [degrees_C, ← bot_eq_zero, sup_bot_eq]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees (X s) ≤ {s}
[PROOFSTEP]
exact degrees_X' _
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ indicator c ∈ restrictDegree σ K (Fintype.card K - 1)
[PROOFSTEP]
rw [mem_restrictDegree_iff_sup, indicator]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
[PROOFSTEP]
intro n
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (degrees (∏ n : σ, (1 - (X n - ↑C (c n)) ^ (Fintype.card K - 1)))) ≤ Fintype.card K - 1
[PROOFSTEP]
refine' le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq _)
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s : σ, (Fintype.card K - 1) • {s}) = Fintype.card K - 1
[PROOFSTEP]
simp_rw [← Multiset.coe_countAddMonoidHom, (Multiset.countAddMonoidHom n).map_sum, AddMonoidHom.map_nsmul,
  Multiset.coe_countAddMonoidHom, nsmul_eq_mul, Nat.cast_id]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
[PROOFSTEP]
trans
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = ?m.190023
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ?m.190023 = Fintype.card K - 1
K : Type u_1 σ : Type u_2 inst✝² : Fintype K inst✝¹ : Fintype σ inst✝ : CommRing K c : σ → K n : σ ⊢ ℕ
[PROOFSTEP]
refine' Finset.sum_eq_single n _ _
[GOAL]
case refine'_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ (b : σ), b ∈ Finset.univ → b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0
[PROOFSTEP]
intro b _ ne
[GOAL]
case refine'_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n b : σ
a✝ : b ∈ Finset.univ
ne : b ≠ n
⊢ (Fintype.card K - 1) * Multiset.count n {b} = 0
[PROOFSTEP]
simp [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
[GOAL]
case refine'_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ¬n ∈ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
h : ¬n ∈ Finset.univ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = 0
[PROOFSTEP]
exact (h <| Finset.mem_univ _).elim
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1
[PROOFSTEP]
rw [Multiset.count_singleton_self, mul_one]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
⊢ ↑(eval a) (indicator b) = 0
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, Function.funext_iff, not_forall] at h 
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
⊢ ∃ i, a i ≠ b i
[PROOFSTEP]
rwa [Ne, Function.funext_iff, not_forall] at h 
[GOAL]
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ↑(eval a) (indicator b) = 0
[PROOFSTEP]
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self, Finset.prod_eq_zero_iff]
[GOAL]
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ∃ a_1, a_1 ∈ Finset.univ ∧ 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
[PROOFSTEP]
refine' ⟨i, Finset.mem_univ _, _⟩
[GOAL]
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0
[PROOFSTEP]
rw [FiniteField.pow_card_sub_one_eq_one, sub_self]
[GOAL]
case intro.ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0
[PROOFSTEP]
rwa [Ne, sub_eq_zero]
[GOAL]
K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
p q : MvPolynomial σ K
⊢ (fun p e => ↑(eval e) p) (p + q) = (fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q
[PROOFSTEP]
ext x
[GOAL]
case h
K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
p q : MvPolynomial σ K
x : σ → K
⊢ (fun p e => ↑(eval e) p) (p + q) x = ((fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q) x
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
a : K
p : MvPolynomial σ K
⊢ AddHom.toFun
      { toFun := fun p e => ↑(eval e) p,
        map_add' :=
          (_ :
            ∀ (p q : MvPolynomial σ K),
              (fun p e => ↑(eval e) p) (p + q) = (fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q) }
      (a • p) =
    ↑(RingHom.id K) a •
      AddHom.toFun
        { toFun := fun p e => ↑(eval e) p,
          map_add' :=
            (_ :
              ∀ (p q : MvPolynomial σ K),
                (fun p e => ↑(eval e) p) (p + q) = (fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q) }
        p
[PROOFSTEP]
ext e
[GOAL]
case h
K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
a : K
p : MvPolynomial σ K
e : σ → K
⊢ AddHom.toFun
      { toFun := fun p e => ↑(eval e) p,
        map_add' :=
          (_ :
            ∀ (p q : MvPolynomial σ K),
              (fun p e => ↑(eval e) p) (p + q) = (fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q) }
      (a • p) e =
    (↑(RingHom.id K) a •
        AddHom.toFun
          { toFun := fun p e => ↑(eval e) p,
            map_add' :=
              (_ :
                ∀ (p q : MvPolynomial σ K),
                  (fun p e => ↑(eval e) p) (p + q) = (fun p e => ↑(eval e) p) p + (fun p e => ↑(eval e) p) q) }
          p)
      e
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
[PROOFSTEP]
cases nonempty_fintype σ
[GOAL]
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
[PROOFSTEP]
refine' top_unique (SetLike.le_def.2 fun e _ => mem_map.2 _)
[GOAL]
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∃ y, y ∈ restrictDegree σ K (Fintype.card K - 1) ∧ ↑(evalₗ K σ) y = e
[PROOFSTEP]
refine' ⟨∑ n : σ → K, e n • indicator n, _, _⟩
[GOAL]
case intro.refine'_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∑ n : σ → K, e n • indicator n ∈ restrictDegree σ K (Fintype.card K - 1)
[PROOFSTEP]
exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)
[GOAL]
case intro.refine'_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ↑(evalₗ K σ) (∑ n : σ → K, e n • indicator n) = e
[PROOFSTEP]
ext n
[GOAL]
case intro.refine'_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ↑(evalₗ K σ) (∑ n : σ → K, e n • indicator n) n = e n
[PROOFSTEP]
simp only [LinearMap.map_sum, @Finset.sum_apply (σ → K) (fun _ => K) _ _ _ _ _, Pi.smul_apply, LinearMap.map_smul]
[GOAL]
case intro.refine'_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • ↑(evalₗ K σ) (indicator x) n = e n
[PROOFSTEP]
simp only [evalₗ_apply]
[GOAL]
case intro.refine'_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • ↑(eval n) (indicator x) = e n
[PROOFSTEP]
trans
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • ↑(eval n) (indicator x) = ?m.293169
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ?m.293169 = e n
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ K
[PROOFSTEP]
refine' Finset.sum_eq_single n (fun b _ h => _) _
[GOAL]
case refine'_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝¹ : e ∈ ⊤
n b : σ → K
x✝ : b ∈ Finset.univ
h : b ≠ n
⊢ e b • ↑(eval n) (indicator b) = 0
[PROOFSTEP]
rw [eval_indicator_apply_eq_zero _ _ h.symm, smul_zero]
[GOAL]
case refine'_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ¬n ∈ Finset.univ → e n • ↑(eval n) (indicator n) = 0
[PROOFSTEP]
exact fun h => (h <| Finset.mem_univ n).elim
[GOAL]
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ e n • ↑(eval n) (indicator n) = e n
[PROOFSTEP]
rw [eval_indicator_apply_eq_one, smul_eq_mul, mul_one]
[GOAL]
σ K : Type u
inst✝¹ : Fintype K
inst✝ : CommRing K
m : ℕ
⊢ DecidablePred fun x => x ∈ {n | ∀ (i : σ), ↑n i ≤ m}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
σ K : Type u
inst✝¹ : Fintype K
inst✝ : CommRing K
m : ℕ
⊢ DecidablePred fun n => ∀ (i : σ), ↑n i ≤ m
[PROOFSTEP]
infer_instance
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ Module.rank K (↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} →₀ K) = #↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1}
[PROOFSTEP]
rw [rank_finsupp_self']
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ #↑{s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} = #↑{s | ∀ (n : σ), s n < Fintype.card K}
[PROOFSTEP]
refine' Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => _⟩
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
⊢ f ∈ {s | ∀ (n : σ), ↑s n ≤ Fintype.card K - 1} ↔ ↑Finsupp.equivFunOnFinite f ∈ {s | ∀ (n : σ), s n < Fintype.card K}
[PROOFSTEP]
refine' forall_congr' fun n => le_tsub_iff_right _
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
f : σ →₀ ℕ
n : σ
⊢ 1 ≤ Fintype.card K
[PROOFSTEP]
exact Fintype.card_pos_iff.2 ⟨0⟩
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ FiniteDimensional K (R σ K)
[PROOFSTEP]
cases nonempty_fintype σ
[GOAL]
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ FiniteDimensional K (R σ K)
[PROOFSTEP]
exact
  IsNoetherian.iff_fg.1
    (IsNoetherian.iff_rank_lt_aleph0.mpr <| by simpa only [rank_R] using Cardinal.nat_lt_aleph0 (Fintype.card (σ → K)))
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Module.rank K (R σ K) < ℵ₀
[PROOFSTEP]
simpa only [rank_R] using Cardinal.nat_lt_aleph0 (Fintype.card (σ → K))
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ range (evalᵢ σ K) = ⊤
[PROOFSTEP]
rw [evalᵢ, LinearMap.range_comp, range_subtype]
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
[PROOFSTEP]
exact map_restrict_dom_evalₗ K σ
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ ker (evalᵢ σ K) = ⊥
[PROOFSTEP]
cases nonempty_fintype σ
[GOAL]
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ ker (evalᵢ σ K) = ⊥
[PROOFSTEP]
refine' (ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank _).mpr (range_evalᵢ σ K)
[GOAL]
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ FiniteDimensional.finrank K (R σ K) = FiniteDimensional.finrank K ((σ → K) → K)
[PROOFSTEP]
rw [FiniteDimensional.finrank_fintype_fun_eq_card, finrank_R]
[GOAL]
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
p : MvPolynomial σ K
h : ∀ (v : σ → K), ↑(eval v) p = 0
hp : p ∈ restrictDegree σ K (Fintype.card K - 1)
p' : R σ K := { val := p, property := hp }
this : p' ∈ ker (evalᵢ σ K)
⊢ p' = 0
[PROOFSTEP]
rwa [ker_evalₗ, mem_bot] at this 
