noncomputable def reynoldsOperator {k : Type u_1} [Field k] {G : Type u_2} [Group G] [Fintype G] {ι : Type u_3} (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) : MvPolynomial ι k →ₗ[k] MvPolynomial ι k

theorem reynolds_maps_to_invariants {k : Type u_1} [Field k] [CharZero k] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (h : MvPolynomial ι k) : (reynoldsOperator algAct) h ∈ polynomialInvariantSubalgebra k G ι algAct

theorem reynolds_identity_on_invariants {k : Type u_1} [Field k] [CharZero k] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (h : MvPolynomial ι k) (hh : h ∈ polynomialInvariantSubalgebra k G ι algAct) : (reynoldsOperator algAct) h = h

noncomputable def positiveInvariantIdeal {k : Type u_1} [Field k] {G : Type u_3} [Group G] {ι : Type u_4} (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) : Ideal (MvPolynomial ι k)

theorem reynolds_mul_invariant {k : Type u_5} [Field k] [CharZero k] {G : Type u_6} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (h f : MvPolynomial ι k) (hf : f ∈ polynomialInvariantSubalgebra k G ι algAct) : (reynoldsOperator algAct) (h * f) = (reynoldsOperator algAct) h * f

theorem invariant_subalgebra_generated_by_ideal_generators {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (r : ℕ) (f : Fin r → MvPolynomial ι k) (hf_inv : ∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct) (hf_gen : positiveInvariantIdeal algAct = Ideal.span (Set.range f)) (hf_pos : ∀ (i : Fin r), 0 < (f i).totalDegree) (h_deg_pres : ∀ (g : G) (p : MvPolynomial ι k), ((algAct g) p).totalDegree ≤ p.totalDegree) (h_coeff_deg : ∀ q ∈ Ideal.span (Set.range f), q ≠ 0 → ∃ (s : Fin r → MvPolynomial ι k), q = ∑ i : Fin r, s i * f i ∧ ∀ (i : Fin r), s i ≠ 0 → (s i).totalDegree + (f i).totalDegree ≤ q.totalDegree) : polynomialInvariantSubalgebra k G ι algAct = Algebra.adjoin k (Set.range f)

noncomputable def normPoly {k : Type u_1} [Field k] {G : Type u_3} [Group G] [Fintype G] {ι : Type u_4} (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) : Polynomial (MvPolynomial ι k)

theorem normPoly_eval_self {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) : Polynomial.eval x (normPoly algAct x) = 0

theorem normPoly_monic {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) : (normPoly algAct x).Monic

theorem normPoly_coeff_invariant {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) (n : ℕ) (h : G) : (algAct h) ((normPoly algAct x).coeff n) = (normPoly algAct x).coeff n

theorem normPoly_coeffs_subset {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) : ↑(normPoly algAct x).coeffs ⊆ ↑(polynomialInvariantSubalgebra k G ι algAct).toSubring

theorem isIntegral_over_invariants {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (x : MvPolynomial ι k) : IsIntegral (↥(polynomialInvariantSubalgebra k G ι algAct)) x

theorem invariant_subalgebra_fg {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) : (polynomialInvariantSubalgebra k G ι algAct).FG

theorem hilbert_noether_lemma {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {A : Type u_2} [CommRing A] [Algebra k A] {G : Type u_3} [Group G] [Fintype G] (algAct : G →* A ≃ₐ[k] A) (hA_fg : ⊤.FG) : (Subalgebra.invariants G algAct).FG

theorem reynolds_diff_of_groupDiff_mem {k : Type u_5} [Field k] [CharZero k] {G : Type u_6} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_7} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (p : MvPolynomial ι k) (I : Ideal (MvPolynomial ι k)) (h_all : ∀ (w : G), (algAct w) p - p ∈ I) : (reynoldsOperator algAct) p - p ∈ I

theorem positiveInvariantIdeal_stable {k : Type u_5} [Field k] {G : Type u_6} [Group G] {ι : Type u_7} (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (w : G) (f : MvPolynomial ι k) (hf : f ∈ positiveInvariantIdeal algAct) : (algAct w) f ∈ positiveInvariantIdeal algAct

theorem list_prod_diff_mem_ideal {k : Type u_5} [Field k] {G : Type u_6} [Group G] {ι : Type u_7} (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (I : Ideal (MvPolynomial ι k)) (hstable : ∀ (w : G), ∀ f ∈ I, (algAct w) f ∈ I) (p : MvPolynomial ι k) (L : List G) (hL : ∀ g ∈ L, (algAct g) p - p ∈ I) : (algAct L.prod) p - p ∈ I

theorem algHom_sub_dvd_of_X_dvd {ι : Type u_5} [Fintype ι] [DecidableEq ι] {k : Type u_6} [CommRing k] (φ : MvPolynomial ι k →ₐ[k] MvPolynomial ι k) (α : MvPolynomial ι k) (hX : ∀ (i : ι), α ∣ φ (MvPolynomial.X i) - MvPolynomial.X i) (p : MvPolynomial ι k) : α ∣ φ p - p

theorem reflection_hyperplane_linear_form {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_6} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_7} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_8} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (σ : G) (hσ : IsComplexReflection (ρ σ)) : ∃ (α : MvPolynomial ι k), α ≠ 0 ∧ α.IsHomogeneous 1 ∧ α.totalDegree = 1 ∧ (∀ (i : ι), α ∣ (algAct σ) (MvPolynomial.X i) - MvPolynomial.X i) ∧ (∀ (i : ι) (d : ℕ), (MvPolynomial.X i).IsHomogeneous d → ∀ (q : MvPolynomial ι k), (algAct σ) (MvPolynomial.X i) - MvPolynomial.X i = q * α → q.IsHomogeneous (d - 1)) ∧ ∀ (p : MvPolynomial ι k) (d : ℕ), p.IsHomogeneous d → ∀ (q : MvPolynomial ι k), (algAct σ) p - p = q * α → q.IsHomogeneous (d - 1)

theorem reflection_hyperplane_divisibility {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_6} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_7} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_8} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (σ : G) (hσ : IsComplexReflection (ρ σ)) : ∃ (α : MvPolynomial ι k), α ≠ 0 ∧ α.IsHomogeneous 1 ∧ α.totalDegree = 1 ∧ ∀ (p : MvPolynomial ι k), ∃ (q : MvPolynomial ι k), (algAct σ) p - p = q * α ∧ ∀ (d : ℕ), p.IsHomogeneous d → q.IsHomogeneous (d - 1)

theorem reflection_divisibility_quotients {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_6} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_7} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_8} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (_hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (h_relation : ∑ i : Fin m, g i * F i = 0) (σ : G) (hσ : IsComplexReflection (ρ σ)) : ∃ (h : Fin m → MvPolynomial ι k), ∑ i : Fin m, h i * F i = 0 ∧ (∀ (i : Fin m), ∃ (d : ℕ), (h i).IsHomogeneous d) ∧ (∀ (i : Fin m), g i ≠ 0 → (g i).totalDegree ≥ 1 → (h i).totalDegree + 1 ≤ (g i).totalDegree) ∧ (h ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct → (algAct σ) (g ⟨0, hm_pos⟩) - g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct) ∧ (g ⟨0, hm_pos⟩ = 0 → (algAct σ) (g ⟨0, hm_pos⟩) - g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct)

theorem reynolds_invariant_pos_deg_mem_positiveInvariantIdeal {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (_hG : IsComplexReflectionGroup G ρ) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (_hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (_hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (hF1_not_in_invG : ¬∃ (c : { j : Fin m // j ≠ ⟨0, hm_pos⟩ } → MvPolynomial ι k), (∀ (i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }), c i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ F ⟨0, hm_pos⟩ = ∑ i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }, c i * F ↑i) (h_relation : ∑ i : Fin m, g i * F i = 0) : (reynoldsOperator algAct) (g ⟨0, hm_pos⟩) ∈ positiveInvariantIdeal algAct

theorem reflection_single_diff_mem {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_6} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_7} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_8} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (_hG : IsComplexReflectionGroup G ρ) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (_hF1_not_in_invG : ¬∃ (c : { j : Fin m // j ≠ ⟨0, hm_pos⟩ } → MvPolynomial ι k), (∀ (i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }), c i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ F ⟨0, hm_pos⟩ = ∑ i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }, c i * F ↑i) (h_relation : ∑ i : Fin m, g i * F i = 0) (σ : G) (hσ : IsComplexReflection (ρ σ)) (IH : ∀ (g' : Fin m → MvPolynomial ι k), (∀ (i : Fin m), ∃ (d : ℕ), (g' i).IsHomogeneous d) → ∑ i : Fin m, g' i * F i = 0 → (g' ⟨0, hm_pos⟩).totalDegree < (g ⟨0, hm_pos⟩).totalDegree → g' ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct) : (algAct σ) (g ⟨0, hm_pos⟩) - g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct

theorem reflection_group_diff_mem_positiveInvariantIdeal {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_6} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_7} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_8} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (hG : IsComplexReflectionGroup G ρ) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (hF1_not_in_invG : ¬∃ (c : { j : Fin m // j ≠ ⟨0, hm_pos⟩ } → MvPolynomial ι k), (∀ (i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }), c i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ F ⟨0, hm_pos⟩ = ∑ i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }, c i * F ↑i) (h_relation : ∑ i : Fin m, g i * F i = 0) (w : G) : (algAct w) (g ⟨0, hm_pos⟩) - g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct

theorem reynolds_diff_mem_positiveInvariantIdeal {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (hG : IsComplexReflectionGroup G ρ) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (hF1_not_in_invG : ¬∃ (c : { j : Fin m // j ≠ ⟨0, hm_pos⟩ } → MvPolynomial ι k), (∀ (i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }), c i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ F ⟨0, hm_pos⟩ = ∑ i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }, c i * F ↑i) (h_relation : ∑ i : Fin m, g i * F i = 0) : (reynoldsOperator algAct) (g ⟨0, hm_pos⟩) - g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct

theorem complex_reflection_syzygy_lemma {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (hG : IsComplexReflectionGroup G ρ) (m : ℕ) (hm_pos : 0 < m) (F g : Fin m → MvPolynomial ι k) (hF_inv : ∀ (i : Fin m), F i ∈ polynomialInvariantSubalgebra k G ι algAct) (hF_homog : ∀ (i : Fin m), ∃ (d : ℕ), (F i).IsHomogeneous d) (hg_homog : ∀ (i : Fin m), ∃ (d : ℕ), (g i).IsHomogeneous d) (hF1_not_in_invG : ¬∃ (c : { j : Fin m // j ≠ ⟨0, hm_pos⟩ } → MvPolynomial ι k), (∀ (i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }), c i ∈ polynomialInvariantSubalgebra k G ι algAct) ∧ F ⟨0, hm_pos⟩ = ∑ i : { j : Fin m // j ≠ ⟨0, hm_pos⟩ }, c i * F ↑i) (h_relation : ∑ i : Fin m, g i * F i = 0) : g ⟨0, hm_pos⟩ ∈ positiveInvariantIdeal algAct

def IsMinimalGeneratingSet {k : Type u_1} [Field k] {ι : Type u_4} (r : ℕ) (f : Fin r → MvPolynomial ι k) (I : Ideal (MvPolynomial ι k)) : Prop

theorem pderiv_aeval_chain_rule {k' : Type u_5} [CommRing k'] {σ' : Type u_6} {τ' : Type u_7} [DecidableEq σ'] [Fintype σ'] (h : MvPolynomial σ' k') (g : σ' → MvPolynomial τ' k') (κ : τ') : (MvPolynomial.pderiv κ) ((MvPolynomial.aeval g) h) = ∑ j : σ', (MvPolynomial.aeval g) ((MvPolynomial.pderiv j) h) * (MvPolynomial.pderiv κ) (g j)

theorem sum_X_mul_pderiv_eq {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (r : ℕ) (f : Fin r → MvPolynomial ι k) (d : Fin r → ℕ) (a : Fin r → MvPolynomial ι k) (b : Fin r → ι → MvPolynomial ι k) (hf_homog : ∀ (j : Fin r), (f j).IsHomogeneous (d j)) (heq : ∀ (κ : ι), ∑ j : Fin r, a j * (MvPolynomial.pderiv κ) (f j) = ∑ j : Fin r, b j κ * f j) : ∑ j : Fin r, d j • (a j * f j) = ∑ j : Fin r, (∑ κ : ι, MvPolynomial.X κ * b j κ) * f j

theorem quasi_homogeneous_wlog_homogeneity {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {ι : Type u_6} [Fintype ι] [DecidableEq ι] {r : ℕ} (f : Fin r → MvPolynomial ι k) (d : Fin r → ℕ) (hf_homog : ∀ (j : Fin r), (f j).IsHomogeneous (d j)) (p : MvPolynomial (Fin r) k) (hp : (MvPolynomial.aeval f) p = 0) (hp_ne : p ≠ 0) (i : Fin r) : ∃ (dg : ℕ), (↑(d i) * (MvPolynomial.aeval f) ((MvPolynomial.pderiv i) p)).IsHomogeneous dg

theorem euler_degree_argument_gives_membership {k : Type u_5} [Field k] [CharZero k] [IsAlgClosed k] {ι : Type u_6} [Fintype ι] [DecidableEq ι] {r : ℕ} (hr_pos : 0 < r) (f : Fin r → MvPolynomial ι k) (d : Fin r → ℕ) (hd_pos : ∀ (j : Fin r), 0 < d j) (hf_homog : ∀ (j : Fin r), (f j).IsHomogeneous (d j)) (hf_min : IsMinimalGeneratingSet r f (Ideal.span (Set.range f))) (a : Fin r → MvPolynomial ι k) (h_euler : ∑ j : Fin r, ↑(d j) * a j * f j = 0) (h_g0_in : ↑(d ⟨0, hr_pos⟩) * a ⟨0, hr_pos⟩ ∈ Ideal.span (Set.range f)) : ∃ (j : Fin r), f j ∈ Ideal.span (Set.range fun (i : { i : Fin r // i ≠ j }) => f ↑i)

theorem minimal_generators_algebraically_independent {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {V : Type u_2} [AddCommGroup V] [Module k V] [FiniteDimensional k V] {G : Type u_3} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (ρ : G →* V ≃ₗ[k] V) (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (hG : IsComplexReflectionGroup G ρ) (r : ℕ) (f : Fin r → MvPolynomial ι k) (d : Fin r → ℕ) (hd_pos : ∀ (j : Fin r), 0 < d j) (hf_homog : ∀ (j : Fin r), (f j).IsHomogeneous (d j)) (hf_inv : ∀ (i : Fin r), f i ∈ polynomialInvariantSubalgebra k G ι algAct) (hf_min : IsMinimalGeneratingSet r f (positiveInvariantIdeal algAct)) : AlgebraicIndependent k f

noncomputable def jacobianMatrixAt {k : Type u_1} [Field k] {ι : Type u_3} (y : ι → MvPolynomial ι k) (u : ι → k) : Matrix ι ι k

theorem eval_algAct_eq_eval_actPoint {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (g : G) (w : ι → k) (f : MvPolynomial ι k) : (MvPolynomial.eval w) ((algAct g) f) = (MvPolynomial.eval fun (i : ι) => (MvPolynomial.eval w) ((algAct g) (MvPolynomial.X i))) f

theorem mv_polynomial_disjoint_separation {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (S T : Finset (ι → k)) (hST : Disjoint S T) : ∃ (p : MvPolynomial ι k), (∀ w ∈ S, (MvPolynomial.eval w) p = 0) ∧ ∀ w ∈ T, (MvPolynomial.eval w) p = 1

theorem maximal_ideals_invariants_bij_orbits {k : Type u_1} [Field k] [CharZero k] [IsAlgClosed k] {G : Type u_2} [Group G] [Fintype G] [DecidableEq G] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (algAct : G →* MvPolynomial ι k ≃ₐ[k] MvPolynomial ι k) (u v : ι → k) : (∀ f ∈ polynomialInvariantSubalgebra k G ι algAct, (MvPolynomial.eval u) f = (MvPolynomial.eval v) f) ↔ ∃ (g : G), ∀ (i : ι), (MvPolynomial.eval v) ((algAct g) (MvPolynomial.X i)) = u i

def IsProductOfReflections {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] {G : Type u_3} [Group G] (ρ : G →* V ≃ₗ[k] V) (g : G) : Prop