theorem Demazure.demazure_order_two {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (Demazure.Demazure i) ((Demazure.Demazure i) p) = 0

theorem Demazure.demazure_commutes_adjacent {n : ℕ} (i : Fin n) (h : ↑i + 1 < n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (⇑(Demazure.Demazure i) ∘ ⇑(Demazure.Demazure ⟨↑i + 1, h⟩) ∘ ⇑(Demazure.Demazure i)) p = (⇑(Demazure.Demazure ⟨↑i + 1, h⟩) ∘ ⇑(Demazure.Demazure i) ∘ ⇑(Demazure.Demazure ⟨↑i + 1, h⟩)) p

theorem Demazure.demazure_commutes_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : (⇑(Demazure.Demazure i) ∘ ⇑(Demazure.Demazure j)) p = (⇑(Demazure.Demazure j) ∘ ⇑(Demazure.Demazure i)) p

theorem Demazure.demazure_mul_monomial_non_adjacent {n : ℕ} (i : Fin n) (j : Fin n) (h : Demazure.NonAdjacent i j) (p : MvPolynomial (Fin (n + 1)) ℂ) : (Demazure.Demazure i) (p * MvPolynomial.X j.castSucc) = (Demazure.Demazure i) p * MvPolynomial.X j.castSucc

theorem Demazure.demazure_mul_monomial_adjacent {n : ℕ} (i : Fin n) (h : ↑i + 1 < n) (p : MvPolynomial (Fin (n + 1)) ℂ) : (Demazure.Demazure i) (p * MvPolynomial.X i.castSucc) = (Demazure.Demazure i) p * MvPolynomial.X i.succ + p

theorem Demazure.demazure_mul_symm {n : ℕ} (i : Fin n) (g : MvPolynomial (Fin (n + 1)) ℂ) (f : MvPolynomial (Fin (n + 1)) ℂ) (h : g.IsSymmetric) : (Demazure.Demazure i) (g * f) = g * (Demazure.Demazure i) f

def Demazure.Dem {n : ℕ} (i : Fin n) : MvPolynomial (Fin (n + 1)) ℂ →ₗ[↥(MvPolynomial.symmetricSubalgebra (Fin (n + 1)) ℂ)] MvPolynomial (Fin (n + 1)) ℂ

Equations

• Demazure.Dem i = { toFun := Demazure.DemazureFun i, map_add' := ⋯, map_smul' := ⋯ }