PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Algebra.MvPolynomial.Basic
public import Mathlib.Algebra.MvPolynomial.CommRing
public import Mathlib.Tactic.Ring

Charge balancing for polynomials

If the variables of a polynomial carry charges under a phase (here a single element c of infinite order), then invariance under the simultaneous phase rotation Xᵢ ↦ c^{wᵢ} Xᵢ forces every monomial to be charge balanced (net charge zero). This is the algebraic content of the statement that a gauge invariant potential, restricted to a slice on which the gauge torus acts diagonally, can only contain charge-balanced monomials.

@[expose] public section

Charge balancing. If each variable Xᵢ carries an integer charge w i, c is a phase of infinite order, and the polynomial f is invariant under the charge rotation Xᵢ ↦ c^{wᵢ} Xᵢ, then every monomial with nonzero net charge has vanishing coefficient.


lemma coeff_eq_zero_of_charge_ne_zero {σ K : Type*} [Field K] (w : σ → ℤ) (c : K) (hc : c ≠ 0)
    (hroot : ∀ n : ℤ, c ^ n = 1 → n = 0) {f : MvPolynomial σ K}
    (hf : aeval (fun i => C (c ^ (w i)) * X i) f = f) {m : σ →₀ ℕ}
    (hm : ∑ i ∈ m.support, (m i : ℤ) * w i ≠ 0) :
    coeff m f = 0 := byσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0⊢ coeff m f = 0
  classical
  have key := coeff_aeval_diag (fun i => c ^ (w i)) f mσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m ((aeval fun i => C (c ^ w i) * X i) f) = (m.prod fun i k => (c ^ w i) ^ k) * coeff m f⊢ coeff m f = 0
  rw [hfσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m f⊢ coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m f⊢ coeff m f = 0] at keyσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m f⊢ coeff m f = 0
  have hgen : ∀ s : Finset σ, ∏ i ∈ s, (c ^ (w i)) ^ (m i)
      = c ^ (∑ i ∈ s, (m i : ℤ) * w i) := by
    intro sσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fs:Finset σ⊢ ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w iσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
    induction s using Finset.induction with
    | empty =>emptyσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m f⊢ ∏ i ∈ ∅, (c ^ w i) ^ m i = c ^ ∑ i ∈ ∅, ↑(m i) * w iσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 simpAll goals completed! 🐙σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
    | @insert x t hx ih =>insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ ∏ i ∈ insert x t, (c ^ w i) ^ m i = c ^ ∑ i ∈ insert x t, ↑(m i) * w iσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
      rw [Finset.prod_insert hx,insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * ∏ x ∈ t, (c ^ w x) ^ m x = c ^ ∑ i ∈ insert x t, ↑(m i) * w iinsertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 Finset.sum_insert hx,insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * ∏ x ∈ t, (c ^ w x) ^ m x = c ^ (↑(m x) * w x + ∑ x ∈ t, ↑(m x) * w x)insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 ih,insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x + ∑ x ∈ t, ↑(m x) * w x)insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 zpow_add₀ hcinsertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xinsertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0]insertσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x * c ^ ∑ i ∈ t, ↑(m i) * w i = c ^ (↑(m x) * w x) * c ^ ∑ x ∈ t, ↑(m x) * w xσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
      congr 1insert.e_aσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ m x = c ^ (↑(m x) * w x)σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
      rw [← zpow_natCast (c ^ w x) (m x),insert.e_aσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ (c ^ w x) ^ ↑(m x) = c ^ (↑(m x) * w x)σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 ← zpow_mul,insert.e_aσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ c ^ (w x * ↑(m x)) = c ^ (↑(m x) * w x)σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 mul_comminsert.e_aσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fx:σt:Finset σhx:x ∉ tih:∏ i ∈ t, (c ^ w i) ^ m i = c ^ ∑ i ∈ t, ↑(m i) * w i⊢ c ^ (↑(m x) * w x) = c ^ (↑(m x) * w x)σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0]σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (m.prod fun i k => (c ^ w i) ^ k) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
  rw [Finsupp.prod,σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (∏ a ∈ m.support, (c ^ w a) ^ m a) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0 hgenσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0] at keyσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w i⊢ coeff m f = 0
  have hne : c ^ (∑ i ∈ m.support, (m i : ℤ) * w i) ≠ 1 := fun h => hm (hroot _ h)σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1⊢ coeff m f = 0
  have h2 : (1 - c ^ (∑ i ∈ m.support, (m i : ℤ) * w i)) * coeff m f = 0 := by
    rw [sub_mul,σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1⊢ 1 * coeff m f - (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0 one_mul,σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1⊢ coeff m f - (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0 ← key,σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1⊢ coeff m f - coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0 sub_selfσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1⊢ 0 = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0]σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0σ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0⊢ coeff m f = 0
  rcases mul_eq_zero.mp h2 with h | hinlσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0h:1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i = 0⊢ coeff m f = 0inrσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0h:coeff m f = 0⊢ coeff m f = 0
  ·inlσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0h:1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i = 0⊢ coeff m f = 0 exact absurd (sub_eq_zero.mp h).symm hneAll goals completed! 🐙
  ·inrσ:Type u_1K:Type u_2inst✝:Field Kw:σ → ℤc:Khc:c ≠ 0hroot:∀ (n : ℤ), c ^ n = 1 → n = 0f:MvPolynomial σ Khf:(aeval fun i => C (c ^ w i) * X i) f = fm:σ →₀ ℕhm:∑ i ∈ m.support, ↑(m i) * w i ≠ 0key:coeff m f = (c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m fhgen:∀ (s : Finset σ), ∏ i ∈ s, (c ^ w i) ^ m i = c ^ ∑ i ∈ s, ↑(m i) * w ihne:c ^ ∑ i ∈ m.support, ↑(m i) * w i ≠ 1h2:(1 - c ^ ∑ i ∈ m.support, ↑(m i) * w i) * coeff m f = 0h:coeff m f = 0⊢ coeff m f = 0 exact hAll goals completed! 🐙