diff --git a/LeanPool.lean b/LeanPool.lean
index 8166ce5d58..d93936da5c 100644
--- a/LeanPool.lean
+++ b/LeanPool.lean
@@ -130,6 +130,13 @@ import LeanPool.DeadEnds.PrimeTail
 import LeanPool.DeadEnds.RelevantPrimes
 import LeanPool.DeadEnds.Solution
 import LeanPool.DeadEnds.TailEstimates
+import LeanPool.DemazureOperatorsLean
+import LeanPool.DemazureOperatorsLean.Demazure
+import LeanPool.DemazureOperatorsLean.DemazureAux
+import LeanPool.DemazureOperatorsLean.DemazureAuxRelations
+import LeanPool.DemazureOperatorsLean.DemazureRelations
+import LeanPool.DemazureOperatorsLean.Matsumoto
+import LeanPool.DemazureOperatorsLean.StrongExchange
 import LeanPool.DirectedTopologyLean4
 import LeanPool.DirectedTopologyLean4.Constructions
 import LeanPool.DirectedTopologyLean4.CoverLemma
diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean
new file mode 100644
index 0000000000..6ed0ad0ed3
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import LeanPool.DemazureOperatorsLean.Demazure
+import LeanPool.DemazureOperatorsLean.DemazureAux
+import LeanPool.DemazureOperatorsLean.DemazureRelations
+import LeanPool.DemazureOperatorsLean.DemazureAuxRelations
+import LeanPool.DemazureOperatorsLean.StrongExchange
+import LeanPool.DemazureOperatorsLean.Matsumoto
+
+/-!
+# Demazure Operators and Lean
+
+Source: doi:10.1070/RM1973v028n03ABEH001549
+Authors: Óscar Álvarez Sánchez
+Status: verified
+Main declarations: `Demazure.Dem`, `CoxeterSystem.strongExchangeProperty`
+Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory
+MSC: 05E05, 13P10, 20F55
+-/
+
+/-!
+The Demazure-operator declarations are sourced to the BGG Schubert-cells paper
+listed in the project card. The strong-exchange declaration is included as
+supporting Coxeter theory with source metadata from Humphreys' *Reflection Groups
+and Coxeter Groups*. The Matsumoto development is retained as conditional
+auxiliary infrastructure because `CoxeterSystem.matsumoto_reduced` assumes the
+extra `MatsumotoCondition` hypothesis.
+-/
diff --git a/LeanPool/DemazureOperatorsLean/Demazure.lean b/LeanPool/DemazureOperatorsLean/Demazure.lean
new file mode 100644
index 0000000000..6b31d4d413
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/Demazure.lean
@@ -0,0 +1,377 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Function
+import Mathlib.Analysis.Complex.Polynomial.Basic
+import Init.System.IO
+
+import Mathlib.Data.Complex.Basic
+
+import Mathlib.Algebra.Polynomial.Basic
+import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.Algebra.MvPolynomial.Rename
+import Mathlib.Algebra.MvPolynomial.Polynomial
+import Mathlib.RingTheory.MvPolynomial.Basic
+
+import Mathlib.Data.Finsupp.Defs
+
+
+noncomputable section
+open MvPolynomial
+
+namespace Demazure
+
+variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1)
+
+/- In this file we define the Demazure operator directly as a function
+  in the ring of multivariate polynomials -/
+
+/- Prerequisites  -/
+
+/-- The polynomial obtained by swapping the variables indexed by `i` and `j`. -/
+def SwapVariablesFun (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : (MvPolynomial (Fin n) ℂ) :=
+  (renameEquiv ℂ (Equiv.swap i j)) p
+
+@[simp]
+lemma swap_variables_map_zero (i j : Fin n) : SwapVariablesFun i j 0 = 0 := by
+  rw[SwapVariablesFun]
+  have : (0 : MvPolynomial (Fin n) ℂ) = C 0 := by
+    refine C_0.symm
+  rw[this]
+  exact rename_C (Equiv.swap i j) 0
+
+@[simp]
+lemma swap_variables_map_one {i j : Fin n} : SwapVariablesFun i j 1 = 1 := by
+  simp[SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_add {i j : Fin n} : ∀p q :
+    MvPolynomial (Fin n) ℂ,
+    SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q := by
+  intro p q
+  simp[SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_sub {i j : Fin n} : ∀p q :
+    MvPolynomial (Fin n) ℂ,
+    SwapVariablesFun i j (p - q) = SwapVariablesFun i j p - SwapVariablesFun i j q := by
+  intro p q
+  simp[SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_mul {i j : Fin n} : ∀p q :
+    MvPolynomial (Fin n) ℂ,
+    SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by
+  intro p q
+  simp[SwapVariablesFun]
+
+lemma swap_variables_mul' (i j : Fin n) : ∀p q :
+    MvPolynomial (Fin n) ℂ,
+    SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by
+  intro p q
+  simp[SwapVariablesFun]
+
+lemma swap_variables_mul'' {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} :
+ SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by
+  simp[SwapVariablesFun]
+
+lemma swap_variables_add'' {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} :
+ SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q := by
+  simp[SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_commutes {i j : Fin n} : ∀r : ℂ, SwapVariablesFun i j (C r) = C r := by
+  intro r
+  simp[SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_order_two {i j : Fin n} {p : MvPolynomial (Fin n) ℂ} :
+  SwapVariablesFun i j (SwapVariablesFun i j p) = p := by
+  rw [SwapVariablesFun, SwapVariablesFun, renameEquiv_apply, renameEquiv_apply, rename_rename]
+  convert rename_id_apply (R := ℂ) p
+  funext k
+  simp
+
+/-- The algebra equivalence swapping the variables indexed by `i` and `j`. -/
+def SwapVariables (i : Fin n) (j : Fin n) :
+    AlgEquiv ℂ (MvPolynomial (Fin n) ℂ) (MvPolynomial (Fin n) ℂ) :=
+  renameEquiv ℂ (Equiv.swap i j)
+
+@[simp]
+lemma swap_variables_apply (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) :
+    SwapVariables i j p = SwapVariablesFun i j p := rfl
+
+/-- The polynomial equation of the unit circle in two variables. -/
+def circleEquation : MvPolynomial (Fin 2) ℂ := X 0 ^ 2 + X 1 ^ 2 - C 1
+
+example : circleEquation = SwapVariables 0 1 circleEquation := by
+  simp [circleEquation, SwapVariables]
+  ring
+
+/- some more properties of swap_variables and others -/
+
+lemma swap_variables_ne_zero (i j : Fin (n + 1)) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ, p ≠ 0 → SwapVariables i j p ≠ 0 := by
+  intro p hp h
+  apply hp
+  rw[← map_zero (SwapVariables i j)] at h
+  apply AlgEquiv.injective (SwapVariables i j)
+  exact h
+
+@[simp]
+lemma swap_variables_first {i j : Fin (n + 1)} : SwapVariablesFun i j (X i) = X j := by
+  simp [SwapVariablesFun]
+
+lemma swap_variables_symmetrical {i j : Fin (n + 1)} {p : MvPolynomial (Fin (n + 1)) ℂ} :
+  SwapVariablesFun i j p = SwapVariablesFun j i p := by
+  simp [SwapVariablesFun, Equiv.swap_comm]
+
+@[simp]
+lemma swap_variables_second {i j : Fin (n + 1)} : SwapVariablesFun i j (X j) = X i := by
+  simp [SwapVariablesFun]
+
+@[simp]
+lemma swap_variables_none {i j k : Fin (n + 1)} (h1 : k ≠ i) (h2 : k ≠ j) :
+SwapVariablesFun i j (X k) = X k := by
+  simp [SwapVariablesFun, h1, h2, Equiv.swap_apply_of_ne_of_ne]
+
+lemma swap_variables_none' {i j k : Fin (n + 1)} {h1 : k ≠ i} {h2 : k ≠ j} :
+SwapVariablesFun i j (X k) = X k := by
+  simp [SwapVariablesFun, h1, h2, Equiv.swap_apply_of_ne_of_ne]
+
+/- Some really specific and technical lemmas-/
+lemma fin_succ_ne_fin_castSucc (i : Fin n) : Fin.succ i ≠ Fin.castSucc i := by
+  apply Fin.val_ne_iff.mp
+  dsimp
+  norm_num
+
+lemma wario_number_one {n : ℕ} {a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} :
+({ val := a, isLt := h } : Fin n) ≠ { val := a', isLt := h' } ↔ a ≠ a' := by
+  rw[ne_eq]
+  rw[ne_eq]
+  apply not_iff_not.mpr
+  exact Fin.mk_eq_mk
+
+
+lemma i_ne_i_plus_1 {i : ℕ} {h : i < n + 1} {h' : i + 1 < n + 1} :
+ ({ val := i, isLt := h } : Fin (n + 1)) ≠ { val := i + 1, isLt := h' } := by
+  rw[wario_number_one]
+  linarith
+
+lemma demazure_denominator_not_null (i : Fin n) :
+    (X (Fin.castSucc i) : MvPolynomial (Fin (n + 1)) ℂ) - X (Fin.succ i) ≠ 0 := by
+  apply MvPolynomial.ne_zero_iff.mpr
+  use Finsupp.single (Fin.succ i) 1
+  rw[MvPolynomial.coeff_sub]
+  rw[MvPolynomial.coeff_X]
+  rw[MvPolynomial.coeff_X']
+  have h : Finsupp.single (Fin.castSucc i) 1 ≠ Finsupp.single (Fin.succ i) 1 := by
+    apply Finsupp.ne_iff.mpr
+    use Fin.succ i
+    simp[fin_succ_ne_fin_castSucc]
+  rw [if_neg h]
+  simp
+
+/- Now we can use these to define the demazure numerator. We distinguish the variable x_i
+ to perform division by (x_i - x_(i+1)) later (only univariable division is supported) -/
+
+/-- The numerator used to define the Demazure operator in one distinguished variable. -/
+def DemazureNumerator (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) :
+    Polynomial (MvPolynomial (Fin n) ℂ) :=
+  let i' : Fin (n + 1) := Fin.castSucc i
+  let i'_plus_1 : Fin (n + 1) := Fin.succ i
+  let numerator := p - SwapVariables i' i'_plus_1 p
+  let numerator_X_i_at_start : MvPolynomial (Fin (n + 1)) ℂ := SwapVariables i' 0 numerator
+  (finSuccEquiv ℂ n) numerator_X_i_at_start
+
+lemma demazure_numerator_add (i : Fin n) : ∀ p q : MvPolynomial (Fin (n + 1)) ℂ,
+  DemazureNumerator i (p + q) = DemazureNumerator i p + DemazureNumerator i q := by
+  intro p q
+  simp [DemazureNumerator, SwapVariables, map_add, sub_eq_add_neg]
+  abel
+
+lemma demazure_numerator_C_mul (i : Fin n) : ∀ (p : MvPolynomial (Fin (n + 1)) ℂ) (r : ℂ),
+ DemazureNumerator i (C r * p) = Polynomial.C (C r) * DemazureNumerator i p := by
+  intro p r
+  simp only [DemazureNumerator, SwapVariables, map_mul, renameEquiv_apply, algHom_C,
+    algebraMap_eq, sub_eq_add_neg, map_add, map_neg, rename_rename]
+  rw [show (MvPolynomial.finSuccEquiv ℂ n) (C r : MvPolynomial (Fin (n + 1)) ℂ) =
+    Polynomial.C (C r) by simp [MvPolynomial.finSuccEquiv_apply]]
+  ring
+
+-- Now we also define the denominator taking the variable x_i as the variable to divide by
+/-- The monic denominator `X - X_i` used in the Demazure division step. -/
+def DemazureDenominator (i : Fin n) : Polynomial (MvPolynomial (Fin n) ℂ)  :=
+  let X_i : MvPolynomial (Fin n) ℂ := MvPolynomial.X i
+  let denominator_X : Polynomial (MvPolynomial (Fin n) ℂ) := (Polynomial.X - Polynomial.C X_i)
+  denominator_X
+
+lemma demazure_denominator_ne_zero : ∀ i : Fin n, DemazureDenominator i ≠ 0 := by
+  intro i
+  simpa [DemazureDenominator] using Polynomial.X_sub_C_ne_zero (X i)
+
+lemma demazure_denominator_monic : ∀ i : Fin n, Polynomial.Monic (DemazureDenominator i) := by
+  intro i
+  simpa [DemazureDenominator] using Polynomial.monic_X_sub_C (X i)
+
+/- the division is exact so the demazure operator is well defined
+(division by polynomials returns just the quotient) -/
+lemma demazure_division_exact : ∀(i : Fin n), ∀(p : MvPolynomial (Fin (n + 1)) ℂ),
+  (DemazureNumerator i p).modByMonic (DemazureDenominator i) = 0 := by
+    intro i p
+    simp only [DemazureNumerator, SwapVariables, renameEquiv_apply, map_sub,
+      rename_rename, finSuccEquiv_apply, coe_eval₂Hom, DemazureDenominator,
+      Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.eval_sub, polynomial_eval_eval₂]
+    apply sub_eq_zero.mpr
+    apply congr_arg Polynomial.C
+    repeat
+      rw[MvPolynomial.eval₂_rename]
+    apply MvPolynomial.eval₂_congr
+    intro j c _ _
+    simp[Equiv.swap_apply_def]
+    by_cases h1 : j = Fin.castSucc i
+    · simp[h1, fin_succ_ne_fin_castSucc i, Fin.succ_ne_zero]
+    by_cases h2 : j = Fin.succ i
+    · simp[h2, fin_succ_ne_fin_castSucc i, Fin.succ_ne_zero]
+    by_cases h3 : j = 0
+    · subst h3
+      simp[h1, h2]
+    simp[h1, h2, h3]
+
+
+/-- The Demazure operator as a function on multivariate polynomials. -/
+def DemazureFun (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : MvPolynomial (Fin (n + 1)) ℂ  :=
+  let numerator := DemazureNumerator i p
+  let denominator := DemazureDenominator i
+  let division := numerator.divByMonic denominator
+  let division_mv : MvPolynomial (Fin (n + 1)) ℂ := (AlgEquiv.symm (finSuccEquiv ℂ n)) division
+  let i' : Fin (n + 1) := Fin.castSucc i
+  SwapVariables i' 0 division_mv
+
+/- Some auxiliary lemmas for the multivariate polynomial ring -/
+lemma poly_mul_cancel {p q r : Polynomial (MvPolynomial (Fin n) ℂ)} (hr : r ≠ 0) :
+    p = q ↔ (r * p) = (r * q) := by
+  constructor
+  · intro h
+    exact congrArg (HMul.hMul r) h
+  · intro h
+    exact mul_left_cancel₀ hr h
+
+lemma poly_cancel_left {p q r : MvPolynomial (Fin n) ℂ} (hr : r ≠ 0) :
+    (r * p) = (r * q) → p = q := by
+  intro h
+  exact mul_left_cancel₀ hr h
+
+lemma poly_div_cancel {p q r : Polynomial (MvPolynomial (Fin n) ℂ)}
+    (hr : Polynomial.Monic r) (hp : p %ₘ r = 0) (hq : q %ₘ r = 0) :
+    p = q ↔ (p /ₘ r) = (q /ₘ r) := by
+  constructor
+  · intro h
+    exact congrArg (fun x => x /ₘ r) h
+  · intro h
+    have div_p : p %ₘ r + r * (p /ₘ r) = p := Polynomial.modByMonic_add_div p r
+    have div_q : q %ₘ r + r * (q /ₘ r) = q := Polynomial.modByMonic_add_div q r
+    rw[hp, zero_add] at div_p
+    rw[hq, zero_add] at div_q
+    rw[← div_p, ← div_q]
+    apply (poly_mul_cancel (Polynomial.Monic.ne_zero hr)).mp h
+
+lemma poly_exact_div_mul_cancel {p q : Polynomial (MvPolynomial (Fin n) ℂ)}
+ (_q_monic : Polynomial.Monic q) (exact_div : p %ₘ q = 0) : q * (p /ₘ q) = p := by
+  nth_rewrite 2 [← sub_zero p]
+  apply eq_sub_of_add_eq
+  rw[add_comm]
+  rw[← exact_div]
+  exact Polynomial.modByMonic_add_div p q
+
+-- since the division is exact, the quotient perfectly divides the numerator
+lemma demazure_division_exact' : ∀(i : Fin n), ∀(p : MvPolynomial (Fin (n + 1)) ℂ),
+    DemazureDenominator i * ((DemazureNumerator i p) /ₘ (DemazureDenominator i)) =
+      DemazureNumerator i p := by
+  intro i p
+  apply poly_exact_div_mul_cancel (demazure_denominator_monic i) (demazure_division_exact i p)
+
+/- Now we prove that the Demazure operator is a linear map directly with the definition.
+  This requires a lot of work to disentangle it -/
+
+lemma demazure_map_add (i : Fin n) : ∀p q : MvPolynomial (Fin (n + 1)) ℂ,
+  DemazureFun i (p + q) = DemazureFun i p + DemazureFun i q := by
+  intro p q
+  simp only [DemazureFun, SwapVariables, renameEquiv_apply]
+  rw[← map_add]
+  apply congr_arg
+  rw[← map_add (AlgEquiv.symm (MvPolynomial.finSuccEquiv ℂ n))
+    (DemazureNumerator i p /ₘ DemazureDenominator i)
+    (DemazureNumerator i q /ₘ DemazureDenominator i)]
+  apply congr_arg
+  apply (poly_mul_cancel (demazure_denominator_ne_zero i)).mpr
+  simp only [mul_add]
+  simp only [demazure_division_exact']
+  exact demazure_numerator_add i p q
+
+lemma demazure_map_smul (i : Fin n) : ∀ (r : ℂ) (p : MvPolynomial (Fin (n + 1)) ℂ),
+  DemazureFun i (r • p) = r • DemazureFun i p := by
+  intro r p
+  simp only [DemazureFun, SwapVariables, smul_eq_C_mul, renameEquiv_apply]
+  nth_rewrite 2 [← rename_C (Equiv.swap (Fin.castSucc i) 0) r]
+  rw[← map_mul]
+  apply congr_arg
+  nth_rewrite 2 [← MvPolynomial.finSuccEquiv_comp_C_eq_C]
+  simp only [RingHom.comp, Nat.succ_eq_add_one, RingHom.coe_coe, RingHom.coe_mk,
+    MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]
+  rw[← map_mul (AlgEquiv.symm (MvPolynomial.finSuccEquiv ℂ n))]
+  apply congr_arg
+  apply (poly_mul_cancel (demazure_denominator_ne_zero i)).mpr
+  rw[← mul_assoc]
+  rw [mul_comm (DemazureDenominator i) (Polynomial.C (C r))]
+  simp only [demazure_division_exact']
+  rw[mul_assoc]
+  rw[demazure_division_exact' i p]
+  exact demazure_numerator_C_mul i p r
+
+/-- The Demazure operator as a complex-linear map. -/
+def DemazureLinear (i : Fin n) :
+    LinearMap (RingHom.id ℂ) (MvPolynomial (Fin (n + 1)) ℂ)
+      (MvPolynomial (Fin (n + 1)) ℂ) where
+  toFun := DemazureFun i
+  map_add' := demazure_map_add i
+  map_smul' := demazure_map_smul i
+
+lemma one_of_div_by_monic_self : ∀ (p : Polynomial (MvPolynomial (Fin n) ℂ))
+    (_h : Polynomial.Monic p), p /ₘ p = 1 := by
+  intro p hp
+  have hmod : p %ₘ p = 0 := (Polynomial.modByMonic_eq_zero_iff_dvd hp).mpr (dvd_refl p)
+  have h := Polynomial.modByMonic_add_div p p
+  rw [hmod, zero_add] at h
+  apply (mul_left_cancel₀ hp.ne_zero)
+  simpa using h
+
+
+-- Example showing that the demazure operator doesn't respect the multiplication
+lemma demazure_not_multiplicative : ∀ (i : Fin n), ∃(p q : MvPolynomial (Fin (n+1)) ℂ),
+  DemazureLinear i (p * q) ≠ DemazureLinear i p * DemazureLinear i q := by
+  intro i
+  use (X (Fin.castSucc i))
+  use C 1
+  simp only [DemazureLinear, mul_one, LinearMap.coe_mk, AddHom.coe_mk, DemazureFun,
+    SwapVariables, DemazureNumerator, renameEquiv_apply, rename_X, Equiv.swap_apply_left,
+    map_sub, Equiv.swap_apply_def, fin_succ_ne_fin_castSucc, ↓reduceIte, Fin.succ_ne_zero,
+    DemazureDenominator, map_one, sub_self, map_zero,
+    Polynomial.zero_divByMonic, mul_zero, ne_eq]
+  rw [MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.finSuccEquiv_X_succ]
+  rw[one_of_div_by_monic_self]
+  · simp
+  · exact Polynomial.monic_X_sub_C (X i)
+
+/- Doing anything with the definition, even simple things, requires a lot of work given
+the complexity of the definition. That's why in DemazureAux.lean we introduce an alternative
+definition that will be the one we actually use for computations -/
+
+end Demazure
+
+end
diff --git a/LeanPool/DemazureOperatorsLean/DemazureAux.lean b/LeanPool/DemazureOperatorsLean/DemazureAux.lean
new file mode 100644
index 0000000000..fcb8d75358
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/DemazureAux.lean
@@ -0,0 +1,422 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import LeanPool.DemazureOperatorsLean.Demazure
+
+
+noncomputable section
+open MvPolynomial
+
+namespace Demazure
+
+variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1)
+
+/- We are going to define the Demazure operator acting on polynomial fractions. For this,
+we first define a structure to represent these fractions, and then we will quotient it by
+the proportionality equivalence relation.
+
+This local quotient is auxiliary proof infrastructure for the Demazure relations below; it
+is not intended as reusable fraction-field or localization theory.
+-/
+
+/-- A numerator-denominator representative for a rational expression in the polynomial ring. -/
+structure PolyFraction' (n : ℕ) where
+  /-- The numerator polynomial. -/
+  numerator : MvPolynomial (Fin (n + 1)) ℂ
+  /-- The denominator polynomial. -/
+  denominator : MvPolynomial (Fin (n + 1)) ℂ
+  /-- The denominator is nonzero. -/
+  denominator_ne_zero : denominator ≠ 0
+
+example : PolyFraction' 2 := ⟨X 0 + X 1, 1, one_ne_zero⟩
+/-- View a polynomial as a fraction with denominator one. -/
+def to_frac (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction' n := ⟨p, 1, one_ne_zero⟩
+
+/-- The proportionality relation on polynomial fractions. -/
+def r (n : ℕ) : PolyFraction' n → PolyFraction' n → Prop :=
+  fun p q => p.numerator * q.denominator = q.numerator * p.denominator
+
+lemma r_equiv : Equivalence (r n) := by
+  constructor
+  · intro p
+    rfl
+  · intro p q h
+    exact h.symm
+  · intro x y z h1 h2
+    change x.numerator * z.denominator = z.numerator * x.denominator
+    change x.numerator * y.denominator = y.numerator * x.denominator at h1
+    change y.numerator * z.denominator = z.numerator * y.denominator at h2
+    by_cases h3 : y.numerator = 0
+    · simp[h3, y.denominator_ne_zero] at h1
+      simp[h3, y.denominator_ne_zero] at h2
+      simp[h1, h2]
+    · apply poly_cancel_left y.denominator_ne_zero
+      apply poly_cancel_left h3
+      ring_nf
+      rw[mul_assoc y.numerator]
+      rw[mul_comm y.denominator x.numerator]
+      rw[h1]
+      rw[mul_comm y.numerator (y.numerator * x.denominator)]
+      rw[mul_assoc]
+      rw[h2]
+      ring_nf
+
+instance s (n : ℕ) : Setoid (PolyFraction' n) where
+  r := r n
+  iseqv := r_equiv
+
+instance has_equiv : HasEquiv (PolyFraction' n) := instHasEquivOfSetoid
+
+lemma equiv_r {a b : PolyFraction' n} : (r n) a b ↔ a ≈ b := by
+  rfl
+
+
+/-- The quotient type of polynomial fractions modulo proportionality. -/
+def PolyFraction (n : ℕ) := (Quotient (s n))
+
+/-- The quotient map from fraction representatives. -/
+def mk (p : PolyFraction' n) : PolyFraction n := Quotient.mk (s n) p
+
+/-- The quotient map from polynomials, viewed as fractions with denominator one. -/
+def mk' (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction n := mk ⟨p, 1, one_ne_zero⟩
+
+
+/- This lemmas enables us to compute the result of a lift of a function applied at a
+ representant class. -/
+lemma lift_r {a : PolyFraction' n} {f : PolyFraction' n → PolyFraction' n}
+    {c : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (mk ∘ f) a₁ = (mk ∘ f) a₂} :
+    Quotient.lift (mk ∘ f) c (mk a) = mk (f a) := by
+  rfl
+@[simp]
+lemma lift2_r {a b : PolyFraction' n}
+    {f : PolyFraction' n → PolyFraction' n → PolyFraction n}
+    {c : ∀ (a₁ b₁ a₂ b₂ : PolyFraction' n), a₁ ≈ a₂ → b₁ ≈ b₂ →
+      f a₁ b₁ = f a₂ b₂} :
+    Quotient.lift₂ f c (mk a) (mk b) = f a b := by
+  rfl
+
+/- Two projections are equal iff the representants are proportional -/
+@[simp]
+lemma mk_eq {a b : PolyFraction' n} :
+    mk a = mk b ↔ a.numerator*b.denominator = a.denominator*b.numerator := by
+  constructor
+  · intro h
+    have hr : a ≈ b := Quotient.exact h
+    rw[← equiv_r] at hr
+    simpa [r, mul_comm] using hr
+  · intro h
+    change Quotient.mk (s n) a = Quotient.mk (s n) b
+    apply Quotient.sound
+    rw[← equiv_r]
+    simpa [r, mul_comm] using h
+
+-- function to get a representant of a fraction
+lemma get_polyfraction_rep (p : PolyFraction n) : ∃p' : PolyFraction' n, mk p' = p := by
+  exact Quotient.exists_rep p
+
+/-- Addition of polynomial-fraction representatives. -/
+def add' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n :=
+  fun p q => ⟨p.numerator * q.denominator + q.numerator * p.denominator,
+    p.denominator * q.denominator, mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩
+
+/-- Addition of representatives followed by the quotient map. -/
+def add_mk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n :=
+  fun p q => mk (add' p q)
+
+lemma add'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ →
+    add_mk a₁ b₁ = add_mk a₂ b₂ := by
+  intro a1 b1 a2 b2 h1 h2
+  simp only [add_mk, add', mk_eq]
+  ring_nf
+  rw[← equiv_r] at h1
+  rw[← equiv_r] at h2
+  change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1
+  change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2
+  rw[mul_comm a1.numerator]
+  rw[mul_assoc b1.denominator]
+  rw[h1]
+  rw[mul_comm b1.numerator]
+  rw[mul_assoc a1.denominator]
+  rw[mul_comm b1.numerator]
+  rw[mul_assoc a1.denominator]
+  rw[mul_assoc a2.denominator]
+  rw[h2]
+  ring_nf
+
+/-- Addition on quotient polynomial fractions. -/
+def add : PolyFraction n → PolyFraction n → PolyFraction n :=
+  fun p q ↦ Quotient.lift₂ (add_mk) (add'_s) p q
+
+-- Enable use of + notation
+instance addition : Add (PolyFraction n) := ⟨add⟩
+instance addition' : Add (PolyFraction' n) := ⟨add'⟩
+
+/-- Subtraction of polynomial-fraction representatives, followed by the quotient map. -/
+def sub' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n :=
+  fun p q ↦ mk ⟨p.numerator * q.denominator - q.numerator * p.denominator,
+    p.denominator * q.denominator, mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩
+
+lemma sub'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ →
+    (sub' a₁ b₁) = (sub' a₂ b₂) := by
+  intro a1 b1 a2 b2 h1 h2
+  simp only [sub', mk_eq]
+  ring_nf
+  rw[← equiv_r] at h1
+  rw[← equiv_r] at h2
+  change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1
+  change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2
+  rw[mul_comm a1.numerator]
+  rw[mul_assoc b1.denominator]
+  rw[h1]
+  rw[mul_comm b1.numerator]
+  rw[mul_assoc a1.denominator]
+  rw[mul_comm b1.numerator]
+  rw[mul_assoc a1.denominator]
+  rw[mul_assoc a2.denominator]
+  rw[h2]
+  ring_nf
+
+/-- Subtraction on quotient polynomial fractions. -/
+def sub : PolyFraction n → PolyFraction n → PolyFraction n :=
+  fun p q ↦ Quotient.lift₂ (sub') (sub'_s) p q
+
+/-- Multiplication of polynomial-fraction representatives. -/
+def mul' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n :=
+  fun p q => ⟨p.numerator * q.numerator, p.denominator * q.denominator,
+    mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩
+
+/-- Multiplication of representatives followed by the quotient map. -/
+def mul_mk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n :=
+  fun p q => mk (mul' p q)
+
+lemma mul'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ →
+    (mul_mk a₁ b₁) = (mul_mk a₂ b₂) := by
+  intro a1 b1 a2 b2 h1 h2
+  simp only [mul_mk, mul', mk_eq]
+  ring_nf
+  rw[← equiv_r] at h1
+  rw[← equiv_r] at h2
+  change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1
+  change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2
+  rw[mul_comm a1.numerator]
+  rw[mul_assoc b1.numerator]
+  rw[h1]
+  rw[mul_comm b1.numerator]
+  rw[mul_assoc (a2.numerator * a1.denominator)]
+  rw[h2]
+  ring_nf
+
+/-- Multiplication on quotient polynomial fractions. -/
+def mul : PolyFraction n → PolyFraction n → PolyFraction n :=
+  fun p q ↦ Quotient.lift₂ (mul_mk) (mul'_s) p q
+
+-- Enable use of * notation
+instance multiplication' : Mul (PolyFraction' n) := ⟨mul'⟩
+instance multiplication : Mul (PolyFraction n) := ⟨mul⟩
+
+/-- The multiplicative identity as a fraction representative. -/
+@[simp]
+def one' : PolyFraction' n where
+  numerator := 1
+  denominator := 1
+  denominator_ne_zero := one_ne_zero
+
+/-- The multiplicative identity as a quotient fraction. -/
+def one : PolyFraction n := mk one'
+
+/-- The additive identity as a fraction representative. -/
+@[simp]
+def zero' : PolyFraction' n where
+  numerator := 0
+  denominator := 1
+  denominator_ne_zero := one_ne_zero
+
+/-- The additive identity as a quotient fraction. -/
+def zero : PolyFraction n := mk zero'
+
+/-- Negation of polynomial-fraction representatives. -/
+def neg' (p : PolyFraction' n) : PolyFraction' n :=
+  ⟨-p.numerator, p.denominator, p.denominator_ne_zero⟩
+
+/-- Negation of representatives followed by the quotient map. -/
+def neg_mk (p : PolyFraction' n) : PolyFraction n := mk (neg' p)
+
+lemma neg_s (n : ℕ) : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (neg_mk a₁) = (neg_mk a₂) := by
+  intro a1 a2 h
+  simp only [neg_mk, neg', mk_eq, neg_mul, mul_neg, neg_inj]
+  ring_nf
+  rw[← equiv_r] at h
+  change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h
+  rw[h]
+  ring_nf
+
+/-- Negation on quotient polynomial fractions. -/
+def neg (p : PolyFraction n) : PolyFraction n := Quotient.lift neg_mk (neg_s n) p
+
+-- some basic properties of these operations
+lemma add_comm (p q : PolyFraction n) : add p q = add q p := by
+  rcases get_polyfraction_rep p with ⟨p', hp⟩
+  rcases get_polyfraction_rep q with ⟨q', hq⟩
+  simp only [add]
+  rw[← hp]
+  rw[← hq]
+  simp[lift2_r]
+  simp[add_mk, add']
+  ring_nf
+
+lemma add_assoc (p q r : PolyFraction n) : add (add p q) r = add p (add q r) := by
+  rcases get_polyfraction_rep p with ⟨p', hp⟩
+  rcases get_polyfraction_rep q with ⟨q', hq⟩
+  rcases get_polyfraction_rep r with ⟨r', hr⟩
+  rw[← hp]
+  rw[← hq]
+  rw[← hr]
+  have hpq : (add (mk p') (mk q')) = mk (add' p' q') := by
+    simp[add, add_mk]
+  have hqr : (add (mk q') (mk r')) = mk (add' q' r') := by
+    simp[add, add_mk]
+  rw[hpq, hqr]
+  simp only [add, lift2_r]
+  simp only [add']
+  apply Quotient.sound
+  apply equiv_r.mp
+  simp[Demazure.r, add']
+  ring_nf
+
+-- We don't prove that it is a ring since we don't need all the properties for our use
+
+/- We directly define the Demazure operator on fractions (even though we proved that
+the result is a polynomial, for the proofs it's better to keep the result as a fraction)-/
+/-- The auxiliary Demazure operator on fraction representatives. -/
+def DemAux' (i : Fin n) : PolyFraction' n → PolyFraction' n := fun p =>
+  ⟨
+    p.numerator * (SwapVariables (Fin.castSucc i) (Fin.succ i) p.denominator) -
+      (SwapVariables (Fin.castSucc i) (Fin.succ i) p.numerator) * p.denominator,
+    p.denominator * (SwapVariables (Fin.castSucc i) (Fin.succ i) p.denominator) *
+      (X (Fin.castSucc i) - X (Fin.succ i)),
+    mul_ne_zero
+      (mul_ne_zero p.denominator_ne_zero
+        (swap_variables_ne_zero (Fin.castSucc i) (Fin.succ i) p.denominator
+          p.denominator_ne_zero))
+      (demazure_denominator_not_null i)
+    ⟩
+
+lemma DemAux_well_defined (i : Fin n) : ∀ (p q : PolyFraction' n),
+    p ≈ q → ((mk ∘ DemAux' i) p) = ((mk ∘ DemAux' i) q) := by
+  intro p q h
+  simp only [Function.comp_apply, DemAux', SwapVariables, renameEquiv_apply, mk_eq]
+  rw[← equiv_r] at h
+  change p.numerator * q.denominator = q.numerator * p.denominator at h
+  let S : MvPolynomial (Fin (n + 1)) ℂ ≃ₐ[ℂ] MvPolynomial (Fin (n + 1)) ℂ :=
+    SwapVariables (Fin.castSucc i) (Fin.succ i)
+  let delta : MvPolynomial (Fin (n + 1)) ℂ := X (Fin.castSucc i) - X (Fin.succ i)
+  have h_swap : S p.numerator * S q.denominator = S q.numerator * S p.denominator := by
+    simpa [S, map_mul] using congrArg S h
+  calc
+    (p.numerator * S p.denominator - S p.numerator * p.denominator) *
+        (q.denominator * S q.denominator * delta) =
+      (p.numerator * q.denominator) * (S p.denominator * S q.denominator * delta) -
+        (S p.numerator * S q.denominator) * (p.denominator * q.denominator * delta) := by
+        ring_nf
+    _ = p.denominator * S p.denominator * delta *
+        (q.numerator * S q.denominator - S q.numerator * q.denominator) := by
+        rw [h, h_swap]
+        ring_nf
+
+/-- The auxiliary Demazure operator on quotient polynomial fractions. -/
+def DemAux (i : Fin n) (p : PolyFraction n) : PolyFraction n :=
+  Quotient.lift (mk ∘ (DemAux' i)) (DemAux_well_defined i) p
+
+/- This definition is equivalent to the direct one on the polynomial ring-/
+lemma demazure_definitions_equivalent' : ∀ i : Fin n, ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+  mk (DemAux' i (to_frac p)) = mk' (DemazureFun i p) := by
+  intro i p
+  simp only [mk', mk_eq, mul_one]
+  simp only [DemAux', to_frac, SwapVariables, renameEquiv_apply, map_one, mul_one, one_mul]
+  have h : DemazureDenominator i * ((DemazureNumerator i p) /ₘ (DemazureDenominator i)) =
+      DemazureNumerator i p := demazure_division_exact' i p
+  apply (SwapVariables (Fin.castSucc i) (0 : Fin (n + 1))).injective
+  apply (MvPolynomial.finSuccEquiv ℂ n).injective
+  change DemazureNumerator i p = (MvPolynomial.finSuccEquiv ℂ n)
+    ((SwapVariables (Fin.castSucc i) 0)
+      ((X (Fin.castSucc i) - X (Fin.succ i)) * DemazureFun i p))
+  rw[← h]
+  simp only [SwapVariables, renameEquiv_apply, map_mul, map_sub, rename_X,
+    Equiv.swap_apply_left, ne_eq, fin_succ_ne_fin_castSucc i, not_false_eq_true,
+    Fin.succ_ne_zero, Equiv.swap_apply_of_ne_of_ne]
+  rw [MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.finSuccEquiv_X_succ]
+  have h3 : DemazureDenominator i = Polynomial.X - Polynomial.C (X i) := by
+    simp [DemazureDenominator]
+  rw[← h3]
+  rw[← poly_mul_cancel (demazure_denominator_ne_zero i)]
+  simp only [DemazureFun, SwapVariables, renameEquiv_apply, rename_rename]
+  rw [show (⇑(Equiv.swap (Fin.castSucc i) 0) ∘ ⇑(Equiv.swap (Fin.castSucc i) 0)) =
+      id by
+    funext k
+    simp]
+  simp
+
+lemma demazure_definitions_equivalent : ∀ i : Fin n, ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+  DemAux i (mk' p) = mk' (DemazureFun i p) := by
+  intro i p
+  rw[mk']
+  simp only [DemAux]
+  rw[lift_r]
+  rw[← demazure_definitions_equivalent' i p]
+  rfl
+
+/- We can prove equalities in the ring of polynomials by reducing to the polynomial fraction case.
+This sets the strategy for proving properties of the Demazure operator:
+
+Prove them for DemAux (in DemazureAuxRelations.lean) and then use these lemmas and
+the equivalence of both operators
+to get the result for Demazure (in DemazureRelations.lean).-/
+lemma eq_zero_of_mk'_zero {p : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = zero ↔ p = 0 := by
+  constructor
+  · intro h
+    simpa [mk', zero] using h
+  · intro h
+    simp[h, mk', zero]
+
+lemma eq_of_eq_mk' {p q : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = mk' q ↔ p = q := by
+  constructor
+  · intro h
+    simpa [mk'] using h
+  · intro h
+    simp[h]
+
+
+/- Some lemmas for interplay between mk and add -/
+@[simp]
+lemma simp_add {p q : PolyFraction n} : p + q = add p q := rfl
+
+lemma mk_add {p q : PolyFraction' n} :  ((mk p) : PolyFraction n) + mk q = mk (p + q) := by
+  have h1 : p+q = add' p q := by rfl
+  have h2 : mk p + mk q = add (mk p) (mk q) := by rfl
+  simp[add, add_mk, add', h1, h2]
+
+lemma mk'_add : ∀ (p q : MvPolynomial (Fin (n + 1)) ℂ), mk' (p + q) = mk' p + mk' q := by
+  simp[mk', add, add_mk, add']
+
+@[simp]
+lemma simp_mul' {p q : PolyFraction' n} :
+    p * q = ⟨p.numerator * q.numerator, p.denominator * q.denominator,
+      mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩ := rfl
+
+@[simp]
+lemma simp_mul {p q : PolyFraction n} : p * q = mul p q := rfl
+
+lemma mk_mul {p q : PolyFraction' n} :  ((mk p) : PolyFraction n) * mk q = mk (p * q) := by
+  have h1 : p*q = mul' p q := by rfl
+  have h2 : mk p * mk q = mul (mk p) (mk q) := by rfl
+  simp[mul, mul_mk, mul']
+
+lemma mk'_mul {p q : MvPolynomial (Fin (n + 1)) ℂ} :  mk' p * mk' q = mk' (p * q) := by
+  simp[mk', mul_mk, mul', mul]
+
+end Demazure
+
+end
diff --git a/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean b/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean
new file mode 100644
index 0000000000..5b1d3170a5
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean
@@ -0,0 +1,215 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import LeanPool.DemazureOperatorsLean.Demazure
+import LeanPool.DemazureOperatorsLean.DemazureAux
+
+noncomputable section
+namespace Demazure
+
+-- Some computations are quite heavy, so we increase the number of heartbeats
+
+open MvPolynomial
+
+variable {n : ℕ} (n_pos : n > 0)
+
+/- Composition relations for Demazure operators -/
+-- Start by proving that the Demazure Operator applied two times is the zero operator
+lemma demaux_order_two : ∀ (i : Fin n) (p : PolyFraction n),
+  (DemAux i  ∘ DemAux i) p = zero := by
+  intro i p
+  rcases get_polyfraction_rep p with ⟨p', rfl⟩
+  dsimp [DemAux]
+  rw[lift_r]
+  rw[lift_r]
+  rw[zero]
+  apply Quotient.sound
+  rw[← equiv_r]
+  simp[r, DemAux']
+  ring
+
+/-- Two indices are non-adjacent when the adjacent transpositions they determine are disjoint. -/
+def NonAdjacent (i j : Fin n) : Prop :=
+ (Fin.castSucc i : Fin (n + 1)) ≠ (Fin.castSucc j : Fin (n + 1)) ∧
+  (Fin.castSucc i : Fin (n + 1)) ≠ (Fin.succ j : Fin (n + 1)) ∧
+  (Fin.succ i : Fin (n + 1)) ≠ (Fin.castSucc j : Fin (n + 1)) ∧
+  (Fin.succ i : Fin (n + 1)) ≠ (Fin.succ j : Fin (n + 1))
+
+lemma equiv_swap_mul_eq_comp {a b c d k : Fin n} :
+(Equiv.swap a b * Equiv.swap c d) k = (Equiv.swap a b ∘ Equiv.swap c d) k := by
+  rfl
+
+lemma renameEquiv_swap_ext {a b c d : Fin n} {R : Type} [CommSemiring R] :
+    rename (Equiv.swap a b * Equiv.swap c d) =
+      (rename (Equiv.swap a b ∘ Equiv.swap c d) :
+        MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin n) R) := by
+  rfl
+
+-- Now prove that demazure operators with non-adjacent indices commute
+lemma transposition_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) :
+  Equiv.swap (Fin.castSucc i) (Fin.succ i) * Equiv.swap (Fin.castSucc j) (Fin.succ j) =
+   Equiv.swap (Fin.castSucc j) (Fin.succ j) * Equiv.swap (Fin.castSucc i) (Fin.succ i) := by
+    rcases h with ⟨h1, h2, h3, h4⟩
+    have h_disjoint :
+        Equiv.Perm.Disjoint (Equiv.swap i.castSucc i.succ)
+          (Equiv.swap j.castSucc j.succ) := by
+      intro k
+      apply or_iff_not_imp_left.mpr
+      intro h
+      rcases Equiv.eq_or_eq_of_swap_apply_ne_self h with h | h
+      · simpa [h] using Equiv.swap_apply_of_ne_of_ne h1 h2
+      · simpa [h] using Equiv.swap_apply_of_ne_of_ne h3 h4
+    rw[Equiv.Perm.Disjoint.commute h_disjoint]
+
+lemma transposition_commutes_non_adjacent' (i j : Fin n) (h : NonAdjacent i j) :
+  Equiv.swap (Fin.castSucc i) (Fin.succ i) ∘ Equiv.swap (Fin.castSucc j) (Fin.succ j) =
+   Equiv.swap (Fin.castSucc j) (Fin.succ j) ∘ Equiv.swap (Fin.castSucc i) (Fin.succ i) := by
+    funext k
+    rw[← equiv_swap_mul_eq_comp]
+    simp[transposition_commutes_non_adjacent i j h]
+
+
+lemma swap_variables_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j)
+    {p : MvPolynomial (Fin (n + 1)) ℂ} :
+    SwapVariablesFun (Fin.castSucc i) (Fin.succ i)
+        (SwapVariablesFun (Fin.castSucc j) (Fin.succ j) p) =
+      SwapVariablesFun (Fin.castSucc j) (Fin.succ j)
+        (SwapVariablesFun (Fin.castSucc i) (Fin.succ i) p) := by
+    dsimp [SwapVariablesFun]
+    simp[transposition_commutes_non_adjacent' i j h]
+
+lemma demaux_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      (DemAux i ∘ DemAux j) (mk' p) = (DemAux j ∘ DemAux i) (mk' p) := by
+  intro p
+  dsimp [DemAux, mk']
+  repeat rw[lift_r]
+  apply mk_eq.mpr
+  simp[DemAux']
+  simp [swap_variables_commutes_non_adjacent i j h]
+  rcases h with ⟨h1, h2, h3, h4⟩
+  simp[h1, h2, h3, h4, h1.symm, h2.symm, h3.symm, h4.symm]
+  ring
+
+/-- Prove some relations between Demazure operators and multiplication by monomials, in the
+adjacent and non-adjacent cases -/
+lemma demaux_mul_monomial_non_adjacent (i j : Fin n) (h : NonAdjacent i j) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      DemAux i (mk' (p * X (Fin.castSucc j))) =
+        (DemAux i (mk' p)) * (mk' (X (Fin.castSucc j))) := by
+  intro p
+  dsimp [DemAux, mul]
+  apply mk_eq.mpr
+  simp[DemAux', mul']
+  rcases h with ⟨h1, h2, h3, h4⟩
+  simp [h1.symm, h3.symm]
+  ring
+
+lemma demaux_mul_monomial_adjacent (i : Fin n) (_h : i + 1 < n) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      (DemAux i (mk' (p * X (Fin.castSucc i)))) =
+        (DemAux i (mk' p)) * (mk' (X (Fin.succ i))) + mk' p := by
+  intro p
+  dsimp [DemAux, mk']
+  repeat rw[lift_r]
+  apply mk_eq.mpr
+  simp[DemAux', mul', add']
+  ring
+
+lemma symm_invariant_swap_variables {i j : Fin n} {g : MvPolynomial (Fin n) ℂ}
+   (h : MvPolynomial.IsSymmetric g) :
+  SwapVariablesFun i j g = g := by
+  dsimp [SwapVariablesFun]
+  exact h (Equiv.swap i j)
+
+/- Now we prove that symmetric polynomials act as scalars -/
+/-- A quotient fraction represented by symmetric numerator and denominator polynomials. -/
+def IsSymmetric (p : PolyFraction n) : Prop := ∃p' : PolyFraction' n,
+ mk p' = p ∧ MvPolynomial.IsSymmetric p'.numerator ∧ MvPolynomial.IsSymmetric p'.denominator
+
+lemma demaux_mul_symm (i : Fin n) (g f : PolyFraction n) (h : IsSymmetric g) :
+  DemAux i (g*f) = g*(DemAux i f) := by
+  rcases h with ⟨g', ⟨rfl, g_num_symm, g_denom_symm⟩⟩
+  rcases get_polyfraction_rep f with ⟨f', rfl⟩
+  rw[mk_mul]
+  dsimp [DemAux]
+  repeat rw[lift_r]
+  rw[← simp_mul']
+  rw[← simp_mul]
+  rw[mk_mul]
+  rw[mk_eq]
+  simp[DemAux']
+  simp[symm_invariant_swap_variables g_num_symm, symm_invariant_swap_variables g_denom_symm]
+  ring
+
+
+-- Prove the relation between demazure operations with adjacent indices
+lemma transposition_commutes_adjacent {i : Fin n} {j : Fin (n + 1)} (h0 : i < n + 1)
+    (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) :
+    Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩
+        (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩
+          (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ j)) =
+      Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩
+        (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩
+          (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ j)) := by
+  simp[Equiv.swap_apply_def]
+  by_cases c0 : j = ⟨i, h0⟩
+  · simp[c0]
+  · by_cases c1 : j = ⟨i + 1, h1⟩
+    · simp[c1]
+    · by_cases c2 : j = ⟨i + 2, h2⟩
+      · simp[c2]
+      · simp[c0,c1,c2]
+
+lemma transposition_commutes_adjacent' {i : Fin n} (h0 : i < n + 1)
+    (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) :
+    (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ ∘
+          (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩) ∘
+        (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩) :
+      Fin (n + 1) → Fin (n + 1)) =
+      Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ ∘
+        (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩) ∘
+          (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩) := by
+  funext j
+  simp[transposition_commutes_adjacent h0 h1 h2]
+
+lemma swap_variables_commutes_adjacent {i : Fin n} {p : MvPolynomial (Fin (n + 1)) ℂ}
+    (h0 : i < n + 1) (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) :
+    SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩
+        (SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩
+          (SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩ p)) =
+      SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩
+        (SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩
+          (SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ p)) := by
+  dsimp [SwapVariablesFun]
+  simp[transposition_commutes_adjacent' h0 h1 h2]
+
+@[simp]
+lemma omg {i : ℕ} : i + 1 + 1 = i + 2 := by
+  ring
+
+-- This takes a lot of time to compute
+lemma demaux_commutes_adjacent (i : Fin n) (h : i + 1 < n) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      (DemAux i ∘ DemAux ⟨i+1, h⟩ ∘ DemAux i) (mk' p) =
+        (DemAux ⟨i+1, h⟩ ∘ DemAux i ∘ DemAux ⟨i+1, h⟩) (mk' p) := by
+  intro p
+  dsimp [DemAux, mk']
+  repeat rw[lift_r]
+  simp[DemAux']
+  simp[Fin.castSucc, Fin.succ, Fin.castAdd, Fin.castLE]
+  have h0 : i < n + 1 := by
+    linarith
+  have h1 : i + 1 < n + 1 := by
+    linarith
+  have h2 : i + 2 < n + 1 := by
+    linarith
+  simp [swap_variables_commutes_adjacent h0 h1 h2]
+  ring
+
+end Demazure
+
+end
diff --git a/LeanPool/DemazureOperatorsLean/DemazureRelations.lean b/LeanPool/DemazureOperatorsLean/DemazureRelations.lean
new file mode 100644
index 0000000000..91caa125fc
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/DemazureRelations.lean
@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import LeanPool.DemazureOperatorsLean.Demazure
+import LeanPool.DemazureOperatorsLean.DemazureAux
+import LeanPool.DemazureOperatorsLean.DemazureAuxRelations
+
+noncomputable section
+open MvPolynomial
+
+namespace Demazure
+
+variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1)
+
+/- Now we prove the relations for the actual Demazure operator on polynomials.
+There isn't a lot of math going on here, we just take the results from DemAux and
+translate them to Demazure-/
+
+-- Demazure operator has order two
+lemma demazure_order_two : ∀ (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ),
+  DemazureLinear i (DemazureLinear i p) = 0 := by
+  intro i p
+  apply eq_zero_of_mk'_zero.mp
+  dsimp [DemazureLinear]
+  rw[← demazure_definitions_equivalent]
+  rw[← demazure_definitions_equivalent]
+  exact demaux_order_two i (mk' p)
+
+-- Demazure operators with adjacent indices have a braid relation
+lemma demazure_commutes_adjacent (i : Fin n) (h : i + 1 < n) : ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+  (DemazureLinear i ∘ DemazureLinear ⟨i+1, h⟩ ∘ DemazureLinear i) p =
+    (DemazureLinear ⟨i+1, h⟩ ∘ DemazureLinear i ∘ DemazureLinear ⟨i+1, h⟩) p := by
+  intro p
+  dsimp [DemazureLinear]
+  apply eq_of_eq_mk'.mp
+  repeat rw[← demazure_definitions_equivalent]
+  apply demaux_commutes_adjacent
+
+-- Demazure operators with non-adjacent indices commute
+lemma demazure_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      (DemazureLinear i ∘ DemazureLinear j) p = (DemazureLinear j ∘ DemazureLinear i) p := by
+  intro p
+  dsimp [DemazureLinear]
+  apply eq_of_eq_mk'.mp
+  repeat rw[← demazure_definitions_equivalent]
+  apply demaux_commutes_non_adjacent
+  exact h
+
+-- Relation between demazure operator and multiplication by non-adjacent monomials
+lemma demazure_mul_monomial_non_adjacent (i j : Fin n) (h : NonAdjacent i j) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      DemazureLinear i (p * X (Fin.castSucc j)) =
+        (DemazureLinear i p) * (X (Fin.castSucc j)) := by
+  intro p
+  dsimp [DemazureLinear]
+  apply eq_of_eq_mk'.mp
+  repeat rw[← demazure_definitions_equivalent]
+  rw[← mk'_mul]
+  rw[← mk'_mul]
+  rw[← demazure_definitions_equivalent]
+  rw[mk'_mul]
+  apply demaux_mul_monomial_non_adjacent i j h
+
+-- Relation between demazure operator and multiplication by adjacent monomial
+lemma demazure_mul_monomial_adjacent (i : Fin n) (h : i + 1 < n) :
+    ∀ p : MvPolynomial (Fin (n + 1)) ℂ,
+      (DemazureLinear i (p * X (Fin.castSucc i))) =
+        (DemazureLinear i p) * (X (Fin.succ i)) + p := by
+  intro p
+  dsimp [DemazureLinear]
+  apply eq_of_eq_mk'.mp
+  rw[mk'_add]
+  rw[← mk'_mul]
+  repeat rw[← demazure_definitions_equivalent]
+  apply demaux_mul_monomial_adjacent i h
+
+-- Symmetric polynomials act as scalars wrt Demazure operators
+lemma demazure_mul_symm (i : Fin n) (g f : MvPolynomial (Fin (n + 1)) ℂ)
+    (h : MvPolynomial.IsSymmetric g) :
+    DemazureLinear i (g*f) = g*(DemazureLinear i f) := by
+  dsimp [DemazureLinear]
+  rw[← eq_of_eq_mk']
+  rw[← demazure_definitions_equivalent]
+  rw [← mk'_mul]
+  rw [← mk'_mul]
+  rw[← demazure_definitions_equivalent]
+  have : IsSymmetric (mk' g) := by
+    dsimp [IsSymmetric]
+    use (to_frac g)
+    dsimp [to_frac]
+    exact ⟨rfl, h, MvPolynomial.IsSymmetric.one⟩
+  exact demaux_mul_symm i (mk' g) (mk' f) this
+
+/- This enables to define the Demazure operator as a linear map over the ring of
+symmetric polynomials, the main result of this project -/
+/-- The Demazure operator as a linear map over the symmetric-polynomial subalgebra. -/
+def Dem (i : Fin n) : LinearMap (RingHom.id (MvPolynomial.symmetricSubalgebra (Fin (n + 1)) ℂ))
+ (MvPolynomial (Fin (n + 1)) ℂ) (MvPolynomial (Fin (n + 1)) ℂ) where
+  toFun := DemazureFun i
+  map_add' := demazure_map_add i
+  map_smul' := by
+    intro r x
+    simp only [RingHom.id_apply]
+    let p : MvPolynomial (Fin (n + 1)) ℂ := r
+    have wah : p = r := by rfl
+    have h : MvPolynomial.IsSymmetric p := by
+      apply (MvPolynomial.mem_symmetricSubalgebra p).mp
+      rw[wah]
+      exact SetLike.coe_mem r
+    exact demazure_mul_symm i p x h
+
+end Demazure
+
+end
diff --git a/LeanPool/DemazureOperatorsLean/Matsumoto.lean b/LeanPool/DemazureOperatorsLean/Matsumoto.lean
new file mode 100644
index 0000000000..f8271831be
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/Matsumoto.lean
@@ -0,0 +1,730 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import LeanPool.DemazureOperatorsLean.StrongExchange
+import Init.Data.List.Erase
+
+namespace CoxeterSystem
+noncomputable section
+
+variable {B : Type}
+variable {W : Type} [Group W]
+variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
+
+instance : DecidableEq W := Classical.typeDecidableEq W
+
+local prefix:100 "s" => cs.simple
+local prefix:100 "π" => cs.wordProd
+local prefix:100 "len" => cs.length
+
+/-- Extra nondegeneracy assumptions used in the Matsumoto theorem development. -/
+class MatsumotoCondition where
+  one_le_M : ∀ i j : B, 1 ≤ M i j
+  alternatingWords_ne_one :
+    ∀ (i j : B) (_ : i ≠ j) (p : ℕ) (_ : 0 < p) (_ : p < M i j),
+      (s i * s j) ^ p ≠ 1
+
+/-- A nil move removes two adjacent equal simple reflections at a given offset. -/
+structure NilMove (cs : CoxeterSystem M W) where
+  /-- The simple reflection index used by the nil move. -/
+  i : B
+  /-- The offset where the nil move is applied. -/
+  p : ℕ
+/-- A braid move replaces a braid word by the opposite braid word at a given offset. -/
+structure BraidMove (cs : CoxeterSystem M W) where
+  /-- The first simple reflection index in the braid word. -/
+  i : B
+  /-- The second simple reflection index in the braid word. -/
+  j : B
+  /-- The offset where the braid move is applied. -/
+  p : ℕ
+
+/-- A Coxeter move is either a nil move or a braid move. -/
+inductive CoxeterMove (cs : CoxeterSystem M W) where
+| nil : cs.NilMove → cs.CoxeterMove
+| braid : cs.BraidMove → cs.CoxeterMove
+
+/-- Apply a nil move to a word. -/
+def apply_nilMove (nm : cs.NilMove) (l : List B) : List B :=
+  match nm with
+  | NilMove.mk i p =>
+    match p with
+    | 0 =>
+      if l.take 2 = [i, i] then
+        l.drop 2
+      else
+        l
+    | p + 1 =>
+      match l with
+      | [] => []
+      | h::t => h :: apply_nilMove (NilMove.mk i p) t
+
+/-- Apply a braid move to a word. -/
+def apply_braidMove (bm : cs.BraidMove) (l : List B) : List B :=
+  match bm with
+  | BraidMove.mk i j p =>
+    match p with
+    | 0 =>
+      if l.take (M i j) = braidWord M i j then
+        braidWord M j i ++ l.drop (M i j)
+      else
+        l
+    | p + 1 =>
+      match l with
+      | [] => []
+      | h::t => h :: apply_braidMove (BraidMove.mk i j p) t
+
+/-- Apply either kind of Coxeter move to a word. -/
+def apply_coxeterMove (cm : cs.CoxeterMove) (l : List B) : List B :=
+  match cm with
+  | CoxeterMove.nil nm => cs.apply_nilMove nm l
+  | CoxeterMove.braid bm => cs.apply_braidMove bm l
+
+theorem nilMove_wordProd (nm : cs.NilMove) (l : List B) : π (cs.apply_nilMove nm l) = π l := by
+  rcases nm with ⟨i, p⟩
+  match p with
+  | 0 =>
+    rw[apply_nilMove]
+    by_cases h : l.take 2 = [i, i]
+    · rw [if_pos h]
+      have h' : l = l.take 2 ++ l.drop 2 := by simp
+      nth_rewrite 2 [h']
+      rw[wordProd_append]
+      rw[h]
+      have h_pair : cs.wordProd [i, i] = 1 := by
+        convert_to cs.wordProd ([i] ++ [i]) = 1
+        rw[wordProd_append]
+        simp
+      rw [h_pair, one_mul]
+    · rw [if_neg h]
+  | p + 1 =>
+    match l with
+    | [] => simp[apply_nilMove]
+    | h::t =>
+      simp only [apply_nilMove, wordProd_cons]
+      rw[nilMove_wordProd (NilMove.mk i p) t]
+
+theorem braidMove_wordProd (bm : cs.BraidMove) (l : List B) :
+    π (cs.apply_braidMove bm l) = π l := by
+  rcases bm with ⟨i, j, p⟩
+  match p with
+    | 0 =>
+      rw[apply_braidMove]
+      by_cases h : List.take (M.M i j) l = braidWord M i j
+      · rw [if_pos h]
+        have h' : l = l.take (M.M i j) ++ l.drop (M.M i j) := by simp
+        nth_rewrite 2 [h']
+        repeat rw[wordProd_append]
+        rw[h]
+        simp[wordProd_braidWord_eq]
+      · rw [if_neg h]
+    | p + 1 =>
+      match l with
+      | [] => simp[apply_braidMove]
+      | h::t =>
+        simp only [apply_braidMove, wordProd_cons]
+        rw[braidMove_wordProd (BraidMove.mk i j p) t]
+
+theorem coxeterMove_wordProd (cm : cs.CoxeterMove) (l : List B) :
+    π (cs.apply_coxeterMove cm l) = π l := by
+  cases cm with
+  | nil nm => exact cs.nilMove_wordProd nm l
+  | braid bm => exact cs.braidMove_wordProd bm l
+
+/-- Apply a list of Coxeter moves to a word from right to left. -/
+def apply_coxeterMove_sequence (cms : List (cs.CoxeterMove)) (l : List B) : List B :=
+  List.foldr (cs.apply_coxeterMove) l cms
+
+example (nm : cs.NilMove) : cs.CoxeterMove := CoxeterMove.nil nm
+
+/-- Apply a sequence of braid moves to a word. -/
+def apply_braidMoveSequence (bms : List (cs.BraidMove)) (l : List B) : List B :=
+  match bms with
+  | [] => l
+  | bm :: bms' => cs.apply_braidMove bm (apply_braidMoveSequence bms' l)
+
+lemma apply_braidMoveSequence_cons (bm : cs.BraidMove) (bms : List (cs.BraidMove))
+    (l : List B) :
+    cs.apply_braidMoveSequence (bm :: bms) l =
+      cs.apply_braidMove bm (cs.apply_braidMoveSequence bms l) := by
+  simp[apply_braidMoveSequence]
+
+lemma cons_of_length_succ {α : Type} (l : List α) {p : ℕ} (h : l.length = p + 1) :
+  ∃ (a : α) (t : List α), l = a :: t ∧ t.length = p := by
+  cases l with
+  | nil =>
+    simp at h
+  | cons a t =>
+    simp at h
+    use a, t
+/-- Shift a braid move one position to the right. -/
+def shift_braidMove (bm : cs.BraidMove) : cs.BraidMove :=
+  match bm with
+  | BraidMove.mk i j p => BraidMove.mk i j (p + 1)
+
+lemma braidMove_cons (bm : cs.BraidMove) (l : List B) (a : B) :
+  a :: cs.apply_braidMove bm l = cs.apply_braidMove (cs.shift_braidMove bm) (a :: l) := by
+  rcases bm with ⟨i, j, p⟩
+  simp[shift_braidMove, apply_braidMove]
+
+lemma braidMoveSequence_cons (bms : List (cs.BraidMove)) (l : List B) (a : B) :
+    a :: cs.apply_braidMoveSequence bms l =
+      cs.apply_braidMoveSequence (List.map cs.shift_braidMove bms) (a :: l) := by
+  induction bms with
+    | nil =>
+       simp[apply_braidMoveSequence]
+    | cons bm bms ih =>
+      rw[apply_braidMoveSequence]
+      rw[cs.braidMove_cons bm]
+      rw[ih]
+      simp[apply_braidMoveSequence_cons]
+
+theorem isReduced_cons (a : B) (l : List B) : cs.IsReduced (a :: l) → cs.IsReduced l := by
+  intro h
+  have h' : l = (a::l).drop 1 := by simp
+  rw[h']
+  exact h.drop 1
+
+lemma leftDescent_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) :
+    cs.IsLeftDescent (π (i :: l)) i := by
+  rw [IsLeftDescent, hr, wordProd_cons, simple_mul_simple_cancel_left, List.length_cons]
+  exact Nat.lt_of_le_of_lt (cs.length_wordProd_le l) (Nat.lt_succ_self l.length)
+
+lemma leftInversion_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) :
+    cs.IsLeftInversion (π (i :: l)) (s i) :=
+  (cs.isLeftInversion_simple_iff_isLeftDescent (π (i :: l)) i).mpr (cs.leftDescent_of_cons i l hr)
+
+theorem alternatingWord_succ_ne_alternatingWord_eraseIdx [MatsumotoCondition cs]
+ (i j : B) (p : ℕ) (hp : p < M i j) (hij : i ≠ j) :
+    ∀ (k : ℕ) (_ : k < p),
+      π (alternatingWord i j (p + 1)) ≠ π (alternatingWord i j p).eraseIdx k := by
+  revert i j
+  induction p with
+  | zero =>
+    intro i j
+    simp[alternatingWord, cs.wordProd_cons]
+  | succ p ih =>
+    intro i j hp hij k hk
+    have hp' : p < M i j := by linarith
+    have hp'' : p < M j i := by
+      rw [M.symmetric]
+      exact hp'
+    have zero_lt_p_succ : 0 < p + 1 := by linarith
+    rw[alternatingWord_succ]
+    nth_rewrite 2 [alternatingWord_succ]
+    simp only [List.concat_eq_append, ne_eq]
+    by_cases h_erase : k < (alternatingWord j i p).length
+    · rw[List.eraseIdx_append_of_lt_length h_erase [j]]
+      intro h_contra
+      simp only [wordProd_append] at h_contra
+      rw[mul_right_cancel_iff] at h_contra
+      have hij' : j ≠ i := by
+        intro h
+        apply hij
+        rw[h]
+      have h_erase' : k < p := by
+        simpa only [length_alternatingWord] using h_erase
+      apply ih j i hp'' hij' k h_erase' h_contra
+    · have h_erase' : (alternatingWord j i p).length ≤ k := by
+        apply Nat.le_of_not_lt
+        exact h_erase
+      rw[List.eraseIdx_append_of_length_le h_erase' [j]]
+      have h_erase_k : [j].eraseIdx (k - (alternatingWord j i p).length) = [] := by
+        have h_index : k - (alternatingWord j i p).length = 0 := by
+          have hk_le : k ≤ p := by omega
+          simpa [length_alternatingWord] using Nat.sub_eq_zero_of_le hk_le
+        rw [h_index]
+        rfl
+      rw[h_erase_k]
+      simp only [List.append_nil, ne_eq]
+      intro h_contra
+      have :
+          cs.wordProd (alternatingWord j i (p + 1) ++ [j]) =
+            cs.wordProd (alternatingWord i j (p + 2)) := by
+        simp[alternatingWord_succ]
+      rw[this] at h_contra
+      simp only [prod_alternatingWord_eq_mul_pow, Order.lt_two_iff, zero_le, Nat.add_div_right,
+        ite_mul, one_mul] at h_contra
+      by_cases p_even : Even p
+      · have p_even' : Even (p + 2) := by
+          exact Even.add p_even (by norm_num : Even 2)
+        rw [if_pos p_even', if_pos p_even] at h_contra
+        apply mul_inv_eq_one.mpr at h_contra
+        rw[← inv_pow (s j * s i) (p/2)] at h_contra
+        simp only [mul_inv_rev, inv_simple] at h_contra
+        rw[← pow_add] at h_contra
+        have : p / 2 + 1 + p / 2 = p + 1 := by
+          have h_half : 2 * (p / 2) = p := Nat.two_mul_div_two_of_even p_even
+          omega
+        rw[this] at h_contra
+        apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra
+        linarith
+      · have p_odd : ¬ Even (p + 2) := by
+          intro h
+          exact p_even ((Nat.even_add.mp h).mpr (by norm_num : Even 2))
+        rw [if_neg p_odd, if_neg p_even] at h_contra
+        apply (@mul_left_cancel_iff _ _ _ (s j) _ _).mpr at h_contra
+        simp only [simple_mul_simple_cancel_left] at h_contra
+        rw[← mul_assoc] at h_contra
+        let p_succ := p / 2 + 1
+        have p_succ_ne_zero : p_succ ≠ 0 := by
+          apply Nat.succ_ne_zero
+        have : (p / 2) = p_succ - 1 := by
+          omega
+        rw[this] at h_contra
+        rw[mul_pow_sub_one p_succ_ne_zero (s j * s i)] at h_contra
+        simp only [add_tsub_cancel_right, p_succ] at h_contra
+        apply mul_inv_eq_one.mpr at h_contra
+        rw[← inv_pow (s j * s i) (p/2 + 1)] at h_contra
+        simp only [mul_inv_rev, inv_simple] at h_contra
+        rw[← pow_add] at h_contra
+        have : p / 2 + 1 + (p / 2 + 1) = p + 1 := by
+          have p_odd_base : Odd p := Nat.not_even_iff_odd.mp p_even
+          calc
+            p / 2 + 1 + (p / 2 + 1) = 1 + p / 2 * 2 + 1 := by ring_nf
+            _ = p + 1 := by rw [Nat.one_add_div_two_mul_two_of_odd p_odd_base]
+        rw[this] at h_contra
+        apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra
+        linarith
+
+lemma prefix_braidWord_aux [MatsumotoCondition cs] (w : W) (l l' : List B) (i j : B)
+    (i_ne_j : i ≠ j) (hil : π(i :: l) = w) (hjl' : π(j :: l') = w)
+    (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) :
+    ∀ (p : ℕ) (_ : p ≤ M i j),
+      ∃ t : List B, π (alternatingWord i j p ++ t) = w ∧
+        cs.IsReduced (alternatingWord i j p ++ t) := by
+  intro p
+  induction p with
+  | zero =>
+    intro _
+    use i :: l
+    constructor
+    · simpa only [alternatingWord, List.nil_append] using hil
+    · simpa only [alternatingWord, List.nil_append] using hr
+  | succ p ih =>
+    intro hp
+    have hp' : p ≤ M i j := by linarith
+    have hp'' : p < M i j := by linarith
+    rcases ih hp' with ⟨t, ht, htr⟩
+    rw[← ht]
+    rw[alternatingWord_succ']
+    by_cases p_even : Even p
+    · rw [if_pos p_even]
+      change ∃ t_1 : List B,
+        s j * π (alternatingWord i j p ++ t_1) = π (alternatingWord i j p ++ t) ∧
+          cs.IsReduced (j :: alternatingWord i j p ++ t_1)
+      suffices ∃ k : Fin t.length, s j * cs.wordProd (alternatingWord i j p ++ t) =
+      cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by
+        rcases this with ⟨k, hk⟩
+        use (t.eraseIdx k)
+        have hw :
+          cs.simple j * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) =
+          cs.wordProd (alternatingWord i j p ++ t)
+        := by
+          rw[← hk]
+          rw [simple_mul_simple_cancel_left]
+        constructor
+        · exact hw
+        · rw [IsReduced]
+          rw [IsReduced] at htr
+          rw [List.cons_append]
+          rw[cs.wordProd_cons]
+          rw[hw]
+          rw[htr]
+          calc
+            (alternatingWord i j p ++ t).length = p + t.length := by
+              rw [List.length_append, length_alternatingWord]
+            _ = (j :: (alternatingWord i j p ++ t.eraseIdx k)).length := by
+              rw [List.length_cons, List.length_append, length_alternatingWord,
+                List.length_eraseIdx_of_lt k.2]
+              have h_t_pos : 0 < t.length :=
+                Nat.lt_of_le_of_lt (Nat.zero_le k) k.2
+              omega
+      have h_left_inversion_j :
+          cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s j) := by
+        rw[ht, ← hjl']
+        apply cs.leftInversion_of_cons j l' hr'
+      rcases cs.strongExchangeProperty (alternatingWord i j p ++ t)
+          ⟨s j, cs.isReflection_simple j⟩ h_left_inversion_j with ⟨k, hk⟩
+      by_cases k_lt_len : k < p
+      · exfalso
+        have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len]
+        rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk
+        simp only [wordProd_append] at hk
+        rw[← mul_assoc] at hk
+        rw[mul_right_cancel_iff] at hk
+        rw[← wordProd_cons] at hk
+        have : j :: alternatingWord i j p = alternatingWord i j (p + 1) := by
+          rw [alternatingWord_succ', if_pos p_even]
+        rw[this] at hk
+        exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k
+          k_lt_len hk
+      · rw [not_lt] at k_lt_len
+        have k_ge_len : (alternatingWord i j p).length ≤ k := by
+          simpa only [length_alternatingWord] using k_lt_len
+        rw[List.eraseIdx_append_of_length_le k_ge_len t] at hk
+        rw[hk]
+        have : k - (alternatingWord i j p).length < t.length := by
+          have kle := k.2
+          simp only [List.length_append, length_alternatingWord] at kle
+          simp only [length_alternatingWord]
+          omega
+        use ⟨k - (alternatingWord i j p).length, this⟩
+    · rw [if_neg p_even]
+      change ∃ t_1 : List B,
+        s i * π (alternatingWord i j p ++ t_1) = π (alternatingWord i j p ++ t) ∧
+          cs.IsReduced (i :: alternatingWord i j p ++ t_1)
+      suffices ∃ k : Fin t.length, s i * cs.wordProd (alternatingWord i j p ++ t) =
+      cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by
+        rcases this with ⟨k, hk⟩
+        use (t.eraseIdx k)
+        have hw :
+            cs.simple i * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) =
+              cs.wordProd (alternatingWord i j p ++ t) := by
+          rw[← hk]
+          rw [simple_mul_simple_cancel_left]
+        constructor
+        · exact hw
+        · rw [IsReduced]
+          rw [IsReduced] at htr
+          rw [List.cons_append]
+          rw[cs.wordProd_cons]
+          rw[hw]
+          rw[htr]
+          calc
+            (alternatingWord i j p ++ t).length = p + t.length := by
+              rw [List.length_append, length_alternatingWord]
+            _ = (i :: (alternatingWord i j p ++ t.eraseIdx k)).length := by
+              rw [List.length_cons, List.length_append, length_alternatingWord,
+                List.length_eraseIdx_of_lt k.2]
+              have h_t_pos : 0 < t.length :=
+                Nat.lt_of_le_of_lt (Nat.zero_le k) k.2
+              omega
+      have h_left_inversion_i :
+          cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s i) := by
+        rw[ht, ← hil]
+        apply cs.leftInversion_of_cons i l hr
+      rcases cs.strongExchangeProperty (alternatingWord i j p ++ t)
+          ⟨s i, cs.isReflection_simple i⟩ h_left_inversion_i with ⟨k, hk⟩
+      by_cases k_lt_len : k < p
+      · exfalso
+        have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len]
+        rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk
+        simp only [wordProd_append] at hk
+        rw[← mul_assoc] at hk
+        rw[mul_right_cancel_iff] at hk
+        rw[← wordProd_cons] at hk
+        have : i :: alternatingWord i j p = alternatingWord i j (p + 1) := by
+          rw [alternatingWord_succ', if_neg p_even]
+        rw[this] at hk
+        exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k
+          k_lt_len hk
+      · rw [not_lt] at k_lt_len
+        have k_ge_len : (alternatingWord i j p).length ≤ k := by
+          simpa only [length_alternatingWord] using k_lt_len
+        rw[List.eraseIdx_append_of_length_le k_ge_len t] at hk
+        rw[hk]
+        have : k - (alternatingWord i j p).length < t.length := by
+          have kle := k.2
+          simp only [List.length_append, length_alternatingWord] at kle
+          simp only [length_alternatingWord]
+          omega
+        use ⟨k - (alternatingWord i j p).length, this⟩
+
+lemma prefix_braidWord [MatsumotoCondition cs] (l l' : List B) (i j : B)
+    (i_ne_j : i ≠ j) (pi_eq : π(i :: l) = π(j :: l'))
+    (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) :
+    ∃ t : List B, π (i :: l) = π (braidWord M i j ++ t) ∧
+      cs.IsReduced (braidWord M i j ++ t) := by
+  have h : M i j ≤ M i j := by linarith
+  have h' : π (j :: l') = π (i :: l) := Eq.symm pi_eq
+  rcases cs.prefix_braidWord_aux (π (i :: l)) l l' i j i_ne_j rfl h' hr hr'
+      (M i j) h with ⟨t, ht, htr⟩
+  use t
+  rw[braidWord]
+  constructor
+  · simp[ht]
+  · exact htr
+
+theorem apply_braidMove_sequence_append (bms bms' : List (cs.BraidMove)) (l : List B) :
+    cs.apply_braidMoveSequence (bms ++ bms') l =
+      cs.apply_braidMoveSequence bms (cs.apply_braidMoveSequence bms' l) := by
+  induction bms with
+  | nil => rfl
+  | cons bm bms ih =>
+    rw [List.cons_append, apply_braidMoveSequence_cons, apply_braidMoveSequence_cons, ih]
+
+theorem concatenate_braidMove_sequences (l l' l'' : List B)
+    (h : ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l')
+    (h' : ∃ bms' : List (cs.BraidMove), cs.apply_braidMoveSequence bms' l' = l'') :
+    ∃ bms'' : List (cs.BraidMove), cs.apply_braidMoveSequence bms'' l = l'' := by
+  rcases h with ⟨bms, hbms⟩
+  rcases h' with ⟨bms', hbms'⟩
+  use bms' ++ bms
+  rw[apply_braidMove_sequence_append, hbms, hbms']
+
+-- move to aux file
+theorem isReduced_of_eq_length (l l' : List B) (h_len : l.length = l'.length) (h_eq : π l = π l')
+   (hr : cs.IsReduced l) : cs.IsReduced l' := by
+  rw[IsReduced]
+  rw[IsReduced] at hr
+  calc
+    len π l' = len π l := by rw[h_eq]
+    _ = l.length := by rw[hr]
+    _ = l'.length := by rw[h_len]
+
+theorem eq_length_of_isReduced (l l' : List B)
+(h_eq : π l = π l') (hr : cs.IsReduced l) (hr' : cs.IsReduced l') :
+    l.length = l'.length := by
+  rw[IsReduced] at hr
+  rw[IsReduced] at hr'
+  calc l.length = len π l := by rw[hr]
+    _ = len π l' := by rw[h_eq]
+    _ = l'.length := by rw[hr']
+
+lemma matsumoto_reduced_inductionStep_of_firstLetterEq (p : ℕ) (l_t l'_t : List B) (i : B)
+    (len_l_t_eq_p : l_t.length = p) (len_l'_t_eq_p : l'_t.length = p)
+    (h_eq : π(i :: l_t) = π(i :: l'_t))
+    (l_reduced : cs.IsReduced (i :: l_t)) (l'_reduced : cs.IsReduced (i :: l'_t))
+    (ih : ∀ (l l' : List B),
+      l.length = p →
+        l'.length = p →
+          cs.IsReduced l →
+            cs.IsReduced l' →
+              cs.wordProd l = cs.wordProd l' →
+                ∃ bms, cs.apply_braidMoveSequence bms l = l') :
+    ∃ bms, cs.apply_braidMoveSequence bms (i :: l_t) = i :: l'_t := by
+  have htr : cs.IsReduced l_t := cs.isReduced_cons i l_t l_reduced
+  have htr' : cs.IsReduced l'_t := cs.isReduced_cons i l'_t l'_reduced
+  have h_prod : π l_t = π l'_t := by
+    apply @mul_left_cancel _ _ _ (cs.simple i) _ _
+    rw[← cs.wordProd_cons i l_t, ← cs.wordProd_cons i l'_t, h_eq]
+  have ⟨bms, ih'⟩ := ih l_t l'_t len_l_t_eq_p len_l'_t_eq_p htr htr' h_prod
+  apply (List.cons_inj_right i).mpr at ih'
+  rw[← ih']
+  rw[braidMoveSequence_cons]
+  use (List.map cs.shift_braidMove bms)
+
+theorem matsumoto_reduced_aux [MatsumotoCondition cs] (p : ℕ) (l l' : List B)
+(len_l_eq_p : l.length = p) (len_l'_eq_p : l'.length = p)
+(l_reduced : cs.IsReduced l) (l'_reduced : cs.IsReduced l') (h_eq : π l = π l') :
+  ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l' := by
+  revert l l'
+  induction p with
+  | zero =>
+    intro l l' hl hl' _ _ _
+    use []
+    change l = l'
+    rw[List.length_eq_zero_iff] at hl
+    rw[List.length_eq_zero_iff] at hl'
+    rw[hl, hl']
+  | succ p ih =>
+    intro l l' len_l_eq_p len_l'_eq_p l_reduced l'_reduced h_eq
+    rcases cons_of_length_succ l len_l_eq_p with ⟨i, l_t, rfl, len_l_t_eq_p⟩
+    rcases cons_of_length_succ l' len_l'_eq_p with ⟨j, l'_t, rfl, len_l'_t_eq_p⟩
+    by_cases first_letter_eq : i = j
+    · rw[first_letter_eq]
+      rw[first_letter_eq] at h_eq
+      rw[first_letter_eq] at l_reduced
+      apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t l'_t j len_l_t_eq_p
+        len_l'_t_eq_p h_eq l_reduced l'_reduced
+      exact ih
+    · obtain ⟨m, hm⟩ : ∃ m : ℕ, M i j = m + 1 := by
+        use M i j - 1
+        simp[MatsumotoCondition.one_le_M cs i j]
+      have hm' : M j i = m + 1 := by
+        rw[M.symmetric]
+        exact hm
+      by_cases m_even : Even m
+      · have j_ne_i : j ≠ i := by
+          intro hji
+          exact first_letter_eq hji.symm
+        obtain ⟨b_tail, hb, b_reduced⟩ :=
+          cs.prefix_braidWord l'_t l_t j i j_ne_i (Eq.symm h_eq) l'_reduced l_reduced
+        have hb' : cs.wordProd (i :: l_t) = cs.wordProd (braidWord M j i ++ b_tail) := by
+          rw[← hb]
+          exact h_eq
+        apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M j i ++ b_tail) (j :: l'_t)
+        · have b_word_cons :
+              (braidWord M j i ++ b_tail) = i :: (alternatingWord j i m ++ b_tail) := by
+            rw[braidWord, hm', alternatingWord_succ', if_pos m_even, List.cons_append]
+          rw[b_word_cons]
+          have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by
+            have h_length :
+                (braidWord M j i ++ b_tail).length = p + 1 := by
+              rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M j i ++ b_tail)
+                hb' l_reduced b_reduced]
+              exact len_l_eq_p
+            rw[b_word_cons] at h_length
+            simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢
+            omega
+          rw[b_word_cons] at hb'
+          rw[b_word_cons] at b_reduced
+          apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t
+            (alternatingWord j i m ++ b_tail) i len_l_t_eq_p b_len_p hb' l_reduced
+            b_reduced ih
+        · apply cs.concatenate_braidMove_sequences (braidWord M j i ++ b_tail)
+            (braidWord M i j ++ b_tail) (j :: l'_t)
+          · use [BraidMove.mk j i 0]
+            rw[apply_braidMoveSequence_cons]
+            change cs.apply_braidMove (BraidMove.mk j i 0) (braidWord M j i ++ b_tail) =
+              braidWord M i j ++ b_tail
+            rw[apply_braidMove]
+            have htake :
+                List.take (M j i) (braidWord M j i ++ b_tail) = braidWord M j i := by
+              rw[← length_alternatingWord j i (M j i)]
+              exact List.take_left
+            have hdrop :
+                List.drop (M j i) (braidWord M j i ++ b_tail) = b_tail := by
+              rw[← length_alternatingWord j i (M j i)]
+              exact List.drop_left
+            rw[if_pos htake, hdrop]
+          · have switch_braidWord :
+                π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by
+              rw[wordProd_append, wordProd_append, cs.wordProd_braidWord_eq j i]
+            rw[switch_braidWord] at hb'
+            have b_reduced' : cs.IsReduced (braidWord M i j ++ b_tail) := by
+              apply cs.isReduced_of_eq_length (braidWord M j i ++ b_tail)
+                (braidWord M i j ++ b_tail)
+              · simp only [List.length_append, length_alternatingWord]
+                rw[M.symmetric]
+              · exact switch_braidWord
+              · exact b_reduced
+            have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M i j ++ b_tail) := by
+              rw[← hb']
+              exact Eq.symm h_eq
+            have b_word_cons :
+                (braidWord M i j ++ b_tail) = j :: (alternatingWord i j m ++ b_tail) := by
+              rw[braidWord, hm, alternatingWord_succ', if_pos m_even, List.cons_append]
+            have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by
+              have h_length :
+                  (braidWord M i j ++ b_tail).length = p + 1 := by
+                rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M i j ++ b_tail)
+                  hb' l'_reduced b_reduced']
+                exact len_l'_eq_p
+              rw[b_word_cons] at h_length
+              simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢
+              omega
+            rw[b_word_cons] at hb'
+            rw[b_word_cons] at b_reduced'
+            rw[b_word_cons]
+            apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p
+              (alternatingWord i j m ++ b_tail) l'_t j b_len_p len_l'_t_eq_p
+              (Eq.symm hb') b_reduced' l'_reduced ih
+      · rcases cs.prefix_braidWord l_t l'_t i j first_letter_eq h_eq l_reduced l'_reduced
+          with ⟨b_tail, hb, b_reduced⟩
+        apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M i j ++ b_tail) (j :: l'_t)
+        · have b_word_cons :
+              (braidWord M i j ++ b_tail) = i :: (alternatingWord i j m ++ b_tail) := by
+            rw[braidWord, hm, alternatingWord_succ', if_neg m_even, List.cons_append]
+          have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by
+            have h_length :
+                (braidWord M i j ++ b_tail).length = p + 1 := by
+              rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M i j ++ b_tail)
+                hb l_reduced b_reduced]
+              exact len_l_eq_p
+            rw[b_word_cons] at h_length
+            simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢
+            omega
+          have i_tail_reduced : cs.IsReduced l_t := by
+            apply cs.isReduced_cons i l_t l_reduced
+          have aword_is_reduced : cs.IsReduced (alternatingWord i j m ++ b_tail) := by
+            apply cs.isReduced_cons i ((alternatingWord i j m) ++ b_tail)
+            rw[← b_word_cons]
+            exact b_reduced
+          have i_tail_eq_aword : π l_t = π (alternatingWord i j m ++ b_tail) := by
+            rw[b_word_cons] at hb
+            rw[wordProd_cons, wordProd_cons] at hb
+            rw[mul_left_cancel_iff] at hb
+            exact hb
+          rcases ih l_t (alternatingWord i j m ++ b_tail) len_l_t_eq_p b_len_p
+            i_tail_reduced aword_is_reduced i_tail_eq_aword with ⟨bms, ih'⟩
+          use (List.map cs.shift_braidMove bms)
+          rw[← braidMoveSequence_cons]
+          suffices cs.apply_braidMoveSequence bms l_t = (alternatingWord i j m ++ b_tail)
+            from by
+              rw[this]
+              rw[← b_word_cons]
+          exact ih'
+        · apply cs.concatenate_braidMove_sequences (braidWord M i j ++ b_tail)
+            (braidWord M j i ++ b_tail) (j :: l'_t)
+          · use [BraidMove.mk i j 0]
+            rw[apply_braidMoveSequence_cons]
+            change cs.apply_braidMove (BraidMove.mk i j 0) (braidWord M i j ++ b_tail) =
+              braidWord M j i ++ b_tail
+            rw[apply_braidMove]
+            have htake :
+                List.take (M i j) (braidWord M i j ++ b_tail) = braidWord M i j := by
+              rw[← length_alternatingWord i j (M i j)]
+              exact List.take_left
+            have hdrop :
+                List.drop (M i j) (braidWord M i j ++ b_tail) = b_tail := by
+              rw[← length_alternatingWord i j (M i j)]
+              exact List.drop_left
+            rw[if_pos htake, hdrop]
+          · have b_word_cons :
+                (braidWord M j i ++ b_tail) = j :: (alternatingWord j i m ++ b_tail) := by
+              rw[braidWord, hm', alternatingWord_succ', if_neg m_even, List.cons_append]
+            have switch_braidWord :
+                π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by
+              rw[wordProd_append, wordProd_append, cs.wordProd_braidWord_eq j i]
+            have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M j i ++ b_tail) := by
+              rw[switch_braidWord]
+              rw[← hb]
+              exact Eq.symm h_eq
+            have b_reduced' : cs.IsReduced (braidWord M j i ++ b_tail) := by
+              apply cs.isReduced_of_eq_length (braidWord M i j ++ b_tail)
+                (braidWord M j i ++ b_tail)
+              · simp only [List.length_append, length_alternatingWord]
+                rw[M.symmetric]
+              · exact Eq.symm switch_braidWord
+              · exact b_reduced
+            have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by
+              have h_length :
+                  (braidWord M j i ++ b_tail).length = p + 1 := by
+                rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M j i ++ b_tail)
+                  hb' l'_reduced b_reduced']
+                exact len_l'_eq_p
+              rw[b_word_cons] at h_length
+              simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢
+              omega
+            have j_tail_reduced : cs.IsReduced l'_t := by
+              apply cs.isReduced_cons j l'_t l'_reduced
+            have aword_is_reduced : cs.IsReduced (alternatingWord j i m ++ b_tail) := by
+              apply cs.isReduced_cons j ((alternatingWord j i m) ++ b_tail)
+              rw[← b_word_cons]
+              exact b_reduced'
+            have j_tail_eq_aword : π (alternatingWord j i m ++ b_tail) = π l'_t := by
+              rw[b_word_cons] at hb'
+              rw[wordProd_cons, wordProd_cons] at hb'
+              rw[mul_left_cancel_iff] at hb'
+              exact Eq.symm hb'
+            rcases ih (alternatingWord j i m ++ b_tail) l'_t b_len_p len_l'_t_eq_p
+              aword_is_reduced j_tail_reduced j_tail_eq_aword with ⟨bms, ih'⟩
+            use (List.map cs.shift_braidMove bms)
+            rw[b_word_cons]
+            rw[← braidMoveSequence_cons]
+            suffices cs.apply_braidMoveSequence bms (alternatingWord j i m ++ b_tail) = l'_t
+              from by
+                rw[this]
+            exact ih'
+
+theorem matsumoto_reduced [MatsumotoCondition cs] (l l' : List B)
+(hr : cs.IsReduced l) (hr' : cs.IsReduced l') (h : π l = π l') :
+  ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l' := by
+  apply cs.matsumoto_reduced_aux (l.length) l l' rfl _ hr hr' h
+  calc
+      l'.length = len (π l') := by
+        rw[IsReduced] at hr'
+        rw[← hr']
+      _ = len (π l) := by rw[h]
+      _ = l.length := by
+        rw[IsReduced] at hr
+        rw[← hr]
+
+end
+
+end CoxeterSystem
diff --git a/LeanPool/DemazureOperatorsLean/StrongExchange.lean b/LeanPool/DemazureOperatorsLean/StrongExchange.lean
new file mode 100644
index 0000000000..908c731ecc
--- /dev/null
+++ b/LeanPool/DemazureOperatorsLean/StrongExchange.lean
@@ -0,0 +1,547 @@
+/-
+Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Óscar Álvarez Sánchez
+-/
+
+import Mathlib.GroupTheory.Coxeter.Inversion
+import Mathlib.Algebra.Group.NatPowAssoc
+import Init.Data.List.Lemmas
+
+namespace CoxeterSystem
+noncomputable section
+
+variable {B : Type}
+variable {W : Type} [Group W]
+variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W)
+
+local prefix:100 "s" => cs.simple
+local prefix:100 "π" => cs.wordProd
+local prefix:100 "len" => cs.length
+
+instance : DecidableEq W := Classical.typeDecidableEq W
+
+/-- The subtype of reflections in a Coxeter system. -/
+def Reflection : Type := {t : W // IsReflection cs t}
+
+/-- The number of times a reflection appears in the left inversion sequence of a word. -/
+def reflection_mem_leftInvSeq_count (l : List B) (t : cs.Reflection) : ℕ :=
+  (cs.leftInvSeq l).count t.1
+
+/-- The parity of the number of occurrences of a reflection in a left inversion sequence. -/
+def reflection_mem_leftInvSeq_parity (l : List B) (t : cs.Reflection) : ZMod 2 :=
+  (reflection_mem_leftInvSeq_count cs l t : ZMod 2)
+
+/-- Conjugate a reflection and keep its reflection witness. -/
+def conj_of_reflection (t : cs.Reflection) (w : W) : cs.Reflection :=
+  ⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩
+
+/-- The parity contribution of a simple reflection to the permutation action. -/
+def eta (i : B) (t : cs.Reflection) : ZMod 2 :=
+  if (s i = t.1) then 1 else 0
+
+lemma eta_eq_eta_of_simpleConj (i : B) (t : cs.Reflection) :
+    cs.eta i t = cs.eta i (cs.conj_of_reflection t (s i)) := by
+  rw [eta, eta]
+  rcases t with ⟨t, ht⟩
+  have : s i = t ↔ s i * t = 1 := by
+    constructor
+    · intro h'
+      rw [h']
+      exact IsReflection.mul_self ht
+    · intro h'
+      apply (mul_left_inj t).mp
+      simpa [IsReflection.mul_self ht] using h'
+  by_cases h : s i = t
+  · simp [h, conj_of_reflection]
+  · simp [this, conj_of_reflection]
+
+/-- The permutation action associated to a simple reflection. -/
+def permutationMap (i : B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 :=
+  fun (t , z) => (cs.conj_of_reflection t (s i), z + cs.eta i t)
+
+theorem permutationMap_orderTwo (i : B) : cs.permutationMap i ∘ cs.permutationMap i = id := by
+  funext ⟨t, z⟩
+  simp only [permutationMap, Function.comp_apply, id_eq]
+  apply Prod.ext
+  · simp[conj_of_reflection, mul_assoc]
+  · rw [← cs.eta_eq_eta_of_simpleConj i t]
+    ring_nf
+    rw [show (2 : ZMod 2) = 0 by decide]
+    simp
+
+lemma leftInvSeq_repeats : ∀ (k : ℕ) (h : k < M i j),
+    (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by
+      simp
+      linarith) =
+    (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by
+      simp
+      linarith) := by
+  intro k h'
+  rw [getElem_leftInvSeq_alternatingWord cs i j (M i j) k (by omega)]
+  rw [getElem_leftInvSeq_alternatingWord cs i j (M i j) (M i j + k) (by omega)]
+  rw[cs.prod_alternatingWord_eq_mul_pow]
+  rw[cs.prod_alternatingWord_eq_mul_pow]
+  have h_odd : Odd (2 * k + 1) := by
+    simp
+  have h_odd' : Odd (2 * ((M i j) + k) + 1) := by
+    simp
+  simp only [Nat.not_even_bit1, ↓reduceIte, mul_right_inj]
+  have two_gt_0 : 2 > 0 := by linarith
+  have h_exp : (2 * k + 1) / 2 = k := by
+    rw[add_comm]
+    rw[Nat.add_mul_div_left 1 k two_gt_0]
+    simp
+  have h_exp' : (2 * ((M i j) + k) + 1) / 2 = (M i j) + k := by
+    rw[add_comm]
+    rw[Nat.add_mul_div_left 1 ((M i j)+k) two_gt_0]
+    simp
+  rw[h_exp, h_exp']
+  rw[NatPowAssoc.npow_add]
+  simp
+
+lemma leftInvSeq_repeats' : ∀ (k : ℕ) (h : k < M i j),
+    (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by
+      simp
+      linarith) =
+    (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by
+      simp
+      linarith) := by
+  intro k h'
+  exact leftInvSeq_repeats cs k h'
+
+lemma nReflectionOccurrences_even_braidWord (t : cs.Reflection) :
+  Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) := by
+  suffices
+      reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t =
+        2 * List.count t.1
+          (List.take (M.M i j)
+            (cs.leftInvSeq (alternatingWord i j (M.M i j * 2)))) from by
+    simp[this]
+  rw [reflection_mem_leftInvSeq_count]
+  suffices
+      cs.leftInvSeq (alternatingWord i j (2 * M i j)) =
+        List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++
+          List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) from by
+    rw[this]
+    simp
+    ring_nf
+  have m_le_two_m : M i j ≤ 2 * M i j := by linarith
+  have length_eq :
+      (cs.leftInvSeq (alternatingWord i j (2 * M i j))).length =
+        (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++
+          List.take (M i j)
+            (cs.leftInvSeq (alternatingWord i j (2 * M i j)))).length := by
+    simp[m_le_two_m]
+    ring_nf
+  apply List.ext_getElem length_eq
+  intro k hk hk'
+  by_cases h : k < M i j
+  · have :
+        k <
+          (List.take (M.M i j)
+            (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length := by
+      simp[h, m_le_two_m]
+    rw[List.getElem_append_left this]
+    rw[List.getElem_take']
+    exact h
+  · have h_k_le : k - M i j < M i j := by
+      have hk_bound : k < 2 * M i j := by
+        simpa using hk
+      have h_ge : M i j ≤ k := Nat.le_of_not_gt h
+      omega
+    have :
+        (List.take (M.M i j)
+          (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length ≤ k := by
+      simp[m_le_two_m]
+      linarith
+    rw[List.getElem_append_right this]
+    rw[List.getElem_take]
+    have take_length :
+        (List.take (M.M i j)
+          (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length = M.M i j := by
+      simp[m_le_two_m]
+    simp only [take_length]
+    rw[← leftInvSeq_repeats' cs (k - M i j) h_k_le]
+    have : M.M i j + (k - M.M i j) = k := by
+      exact Nat.add_sub_of_le (Nat.le_of_not_gt h)
+    simp[this]
+
+lemma parityReflectionOccurrences_braidWord (t : cs.Reflection) :
+  reflection_mem_leftInvSeq_parity cs (alternatingWord i j (2 * M i j)) t = 0 := by
+  suffices Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) from by
+    rw [reflection_mem_leftInvSeq_parity]
+    apply ZMod.natCast_eq_zero_iff_even.mpr this
+  exact nReflectionOccurrences_even_braidWord cs t
+
+lemma alternatingWord_reverse :
+    (alternatingWord i j (2 * p)).reverse = alternatingWord j i (2 * p) := by
+  induction p with
+  | zero =>
+    simp[alternatingWord]
+  | succ p h =>
+    rw [show 2 * (p + 1) = 2 * p + 1 + 1 by ring_nf]
+    rw [alternatingWord_succ]
+    rw [alternatingWord_succ]
+    simp only [List.concat_eq_append, List.reverse_append, List.reverse_singleton,
+      List.singleton_append]
+    rw [h]
+    simp only [alternatingWord_succ', Nat.not_even_bit1, even_two_mul, if_false, if_true]
+
+instance instMul : Mul (cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) where
+  mul := fun f g => f ∘ g
+
+lemma mulDef (f g : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) : f * g = f ∘ g := rfl
+
+instance : Monoid (cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) where
+  one := id
+  mul := (instMul cs).mul
+  one_mul := by
+    intro f
+    funext x
+    suffices (id ∘ f) x = f x from by
+      rw[← this]
+      rfl
+    simp
+  mul_one := by
+    intro f
+    funext x
+    suffices (f ∘ id) x = f x from by
+      rw[← this]
+      rfl
+    simp
+  mul_assoc := by
+    intro f g h
+    funext x
+    repeat rw[mulDef]
+    rfl
+
+/-- The permutation map associated to a word, built by composing simple permutation maps. -/
+def permutationMap_ofList (l : List B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 :=
+  match l with
+  | [] => id
+  | a :: t => cs.permutationMap a * permutationMap_ofList t
+
+lemma isReflection_conj_inv_mul_mul (ht : cs.IsReflection t) (w : W) :
+  cs.IsReflection (w⁻¹ * t * w) := by
+  have : w = w⁻¹⁻¹ := by simp
+  nth_rewrite 2 [this]
+  apply IsReflection.conj ht w⁻¹
+
+lemma permutationMap_ofList_mk_1 (l : List B) :
+  (permutationMap_ofList cs l ⟨t,z⟩).1 = cs.conj_of_reflection t (π l) := by
+  induction l with
+  | nil =>
+    simp[permutationMap_ofList, conj_of_reflection]
+  | cons a l h =>
+    calc
+      (permutationMap_ofList cs (a :: l) (t, z)).1 =
+          ((cs.permutationMap a * permutationMap_ofList cs l) (t, z)).1 := by
+        simp[permutationMap_ofList]
+      _ = (cs.permutationMap a (permutationMap_ofList cs l (t, z))).1 := by rfl
+      _ = cs.conj_of_reflection t (π (a :: l)) := by
+        simp[permutationMap, conj_of_reflection, h, cs.wordProd_cons, mul_assoc]
+
+lemma permutationMap_ofList_mk_2 (l : List B) :
+    (permutationMap_ofList cs l ⟨t,z⟩).2 =
+      z + reflection_mem_leftInvSeq_parity cs l.reverse t := by
+  induction l with
+  | nil =>
+    simp[permutationMap_ofList, reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count]
+  | cons i l h =>
+    rw[permutationMap_ofList, mulDef]
+    change (cs.permutationMap i (permutationMap_ofList cs l (t, z))).2 =
+      z + reflection_mem_leftInvSeq_parity cs (i :: l).reverse t
+    rw [permutationMap]
+    change (permutationMap_ofList cs l (t, z)).2 +
+        cs.eta i (permutationMap_ofList cs l (t, z)).1 =
+      z + reflection_mem_leftInvSeq_parity cs (i :: l).reverse t
+    rw [h]
+    simp only [reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count,
+      List.reverse_cons]
+    rw[← List.concat_eq_append]
+    rw[leftInvSeq_concat]
+    simp only [wordProd_reverse, inv_inv, List.concat_eq_append, List.count_append,
+      Nat.cast_add]
+    suffices
+        cs.eta i (permutationMap_ofList cs l (t, z)).1 =
+          if (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 then 1 else 0 from by
+      rw[this]
+      simp[add_assoc, List.count_singleton]
+    simp only [eta, permutationMap_ofList_mk_1, conj_of_reflection]
+    by_cases h' : (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1
+    · have lhs : cs.simple i = cs.wordProd l * t.1 * (cs.wordProd l)⁻¹ := by
+        rw [← h']
+        simp [mul_assoc]
+      rw [if_pos lhs, if_pos h']
+    · have lhs_ne : ¬cs.simple i = cs.wordProd l * t.1 * (cs.wordProd l)⁻¹ := by
+        intro h''
+        apply h'
+        rw [h'']
+        simp [mul_assoc]
+      rw [if_neg lhs_ne, if_neg h']
+
+lemma permutationMap_ofList_mk (l : List B) (t : cs.Reflection) (z : ZMod 2) :
+  (permutationMap_ofList cs l ⟨t,z⟩) = ⟨cs.conj_of_reflection t (π l),
+   z + reflection_mem_leftInvSeq_parity cs l.reverse t⟩ := by
+  rw[← permutationMap_ofList_mk_1, ← permutationMap_ofList_mk_2]
+
+theorem permutationMap_isLiftable : M.IsLiftable (cs.permutationMap) := by
+  intro i j
+  have h (p : ℕ) :
+      (cs.permutationMap i * cs.permutationMap j) ^ p =
+        permutationMap_ofList cs (alternatingWord i j (2 * p)) := by
+    induction p with
+    | zero =>
+      rfl
+    | succ p h =>
+      rw[pow_succ']
+      rw[h]
+      have : 2 * (p + 1) = 2 * p + 1 + 1 := by ring_nf
+      rw[this]
+      rw[alternatingWord_succ']
+      rw [if_neg (Nat.not_even_bit1 p)]
+      rw[permutationMap_ofList]
+      rw[alternatingWord_succ']
+      rw [if_pos (even_two_mul p)]
+      rw[permutationMap_ofList]
+      simp[mul_assoc]
+  rw[h (M i j)]
+  funext ⟨t, z⟩
+  convert_to permutationMap_ofList cs (alternatingWord i j (2 * M.M i j)) (t, z) = ⟨t,z⟩
+  rw[permutationMap_ofList_mk]
+  apply Prod.ext
+  · simp[conj_of_reflection, cs.prod_alternatingWord_eq_mul_pow]
+  · rw[alternatingWord_reverse]
+    rw[M.symmetric]
+    simp [parityReflectionOccurrences_braidWord (M := M) cs (i := j) (j := i) t]
+
+/-- The homomorphic lift of the simple permutation maps to the Coxeter group. -/
+def permutationMap_lift : W →* cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 :=
+  cs.lift ⟨cs.permutationMap, permutationMap_isLiftable cs⟩
+
+theorem permutationMap_lift_mk_ofList (l : List B) (t : cs.Reflection) (z : ZMod 2) :
+  permutationMap_lift cs (cs.wordProd l) ⟨t,z⟩ = permutationMap_ofList cs l ⟨t,z⟩ := by
+  induction l with
+  | nil =>
+    simp[permutationMap_lift, cs.wordProd_nil, permutationMap_ofList]
+    rfl
+  | cons i l h =>
+    rw[cs.wordProd_cons]
+    rw[permutationMap_ofList]
+    simp only [mulDef, map_mul, Function.comp_apply]
+    rw[← h]
+    simp[permutationMap_lift]
+
+theorem permutationMap_ext (l l' : List B) (t : cs.Reflection) (z : ZMod 2) (h : π l = π l') :
+  permutationMap_ofList cs l ⟨t,z⟩ = permutationMap_ofList cs l' ⟨t,z⟩ := by
+  rw[← permutationMap_lift_mk_ofList]
+  rw[← permutationMap_lift_mk_ofList]
+  simp[h]
+
+/-- The parity of reflection occurrences defined using the lifted permutation action. -/
+def parityReflectionOccurrences_lift (w : W) (t : cs.Reflection) : ZMod 2 :=
+  (permutationMap_lift cs w⁻¹ ⟨t,0⟩).2
+
+theorem parityReflectionOccurrences_lift_mk (l : List B) (t : cs.Reflection) :
+    parityReflectionOccurrences_lift cs (cs.wordProd l) t =
+      reflection_mem_leftInvSeq_parity cs l t := by
+  rw[parityReflectionOccurrences_lift]
+  rw[← wordProd_reverse]
+  rw[permutationMap_lift_mk_ofList cs l.reverse t 0]
+  rw[permutationMap_ofList_mk cs l.reverse t 0]
+  simp
+
+theorem permutationMap_lift_mk (w : W) (t : cs.Reflection) (z : ZMod 2) :
+    permutationMap_lift cs w ⟨t,z⟩ =
+      ⟨⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩,
+        z + parityReflectionOccurrences_lift cs w⁻¹ t⟩ := by
+  obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w
+  apply Prod.ext
+  · simp[permutationMap_lift_mk_ofList, permutationMap_ofList_mk, conj_of_reflection]
+  · simp only [parityReflectionOccurrences_lift, inv_inv]
+    rw[permutationMap_lift_mk_ofList cs l t 0]
+    rw[permutationMap_lift_mk_ofList cs l t z]
+    simp[permutationMap_ofList_mk]
+
+
+theorem parityReflectionOccurrences_ext (l l' : List B) (t : cs.Reflection) (h : π l = π l') :
+  reflection_mem_leftInvSeq_parity cs l t = reflection_mem_leftInvSeq_parity cs l' t := by
+  calc
+    reflection_mem_leftInvSeq_parity cs l t =
+        parityReflectionOccurrences_lift cs (cs.wordProd l) t := by
+      rw[parityReflectionOccurrences_lift_mk]
+    _ = parityReflectionOccurrences_lift cs (cs.wordProd l') t := by rw[h]
+    _ = reflection_mem_leftInvSeq_parity cs l' t := by rw[parityReflectionOccurrences_lift_mk]
+
+lemma odd_iff_parity_eq_one (n : ℕ) : Odd n ↔ (n : ZMod 2) = 1 := by
+  simpa [eq_comm] using (ZMod.natCast_eq_one_iff_odd (n := n)).symm
+
+lemma gt_one_of_odd (n : ℕ) : Odd n → n > 0 := by
+  intro h
+  rcases h with ⟨m, rfl⟩
+  suffices m ≥ 0 from by linarith
+  exact Nat.zero_le m
+
+lemma isInLeftInvSeq_of_parityReflectionOccurrences_eq_one
+    (l : List B) (t : cs.Reflection)
+    (h : reflection_mem_leftInvSeq_parity cs l t = 1) :
+    t.1 ∈ cs.leftInvSeq l := by
+  rw [reflection_mem_leftInvSeq_parity] at h
+  rw [← @odd_iff_parity_eq_one (reflection_mem_leftInvSeq_count cs l t)] at h
+  apply gt_one_of_odd (reflection_mem_leftInvSeq_count cs l t) at h
+  rw[reflection_mem_leftInvSeq_count] at h
+  exact List.count_pos_iff.mp h
+
+lemma isLeftInversion_of_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) :
+  reflection_mem_leftInvSeq_parity cs l t = 1 → cs.IsLeftInversion (cs.wordProd l) t.1 := by
+  intro h
+  rcases cs.exists_isReduced (π l) with ⟨u, u_reduced, hu⟩
+  rw[hu]
+  apply cs.isLeftInversion_of_mem_leftInvSeq u_reduced
+  rw[cs.parityReflectionOccurrences_ext l u t hu] at h
+  exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs u t h
+
+lemma isLeftInversion_of_parityReflectionOccurrences_lift_eq_one (w : W) (t : cs.Reflection) :
+  parityReflectionOccurrences_lift cs w t = 1 → cs.IsLeftInversion w t.1 := by
+  intro h
+  obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w
+  rw[parityReflectionOccurrences_lift_mk] at h
+  apply isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t h
+
+lemma eraseIdx_of_mul_leftInvSeq (l : List B) (t : cs.Reflection) (h : t.1 ∈ cs.leftInvSeq l) :
+  ∃ (k : Fin l.length), t.1 * π l = π (l.eraseIdx k) := by
+    have : ∃ (k : Fin (cs.leftInvSeq l).length), (cs.leftInvSeq l).get k = t.1 := List.get_of_mem h
+    rcases this with ⟨k, hk⟩
+    use ⟨k, by rw[← length_leftInvSeq cs l]; exact k.2⟩
+    rw[← hk]
+    rw[← getD_leftInvSeq_mul_wordProd cs l k]
+    simp [List.getElem?_eq_getElem k.2]
+
+lemma permutationMap_lift_simple (p : B) :
+  permutationMap_lift cs (cs.simple p) = cs.permutationMap p := by
+  simp[permutationMap_lift]
+
+lemma permutationMap_lift_of_reflection (t : cs.Reflection) : ∀ (z : ZMod 2),
+  permutationMap_lift cs t.1 (t, z) = ⟨t, z + 1⟩ := by
+  rcases t with ⟨t, t_refl⟩
+  rcases t_refl with ⟨w, p, rfl⟩
+  obtain ⟨l, _, rfl⟩ := cs.wordProd_surjective w
+  have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) :=
+    IsReflection.conj (isReflection_simple cs p) (cs.wordProd l)
+  induction l with
+  | nil =>
+    simp[permutationMap_lift, permutationMap, conj_of_reflection, eta]
+  | cons i l h =>
+    intro z
+    simp_rw[wordProd_cons cs i l]
+    simp_rw[mul_inv_rev]
+    simp_rw[inv_simple]
+    simp only [permutationMap_lift_simple, mulDef, map_mul, Function.comp_apply]
+    simp only [permutationMap_lift_simple, mulDef, map_mul, Function.comp_apply] at h
+    nth_rewrite 3 [permutationMap]
+    conv_lhs => simp [conj_of_reflection, ← mul_assoc]
+    have :
+        IsReflection cs
+          (cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i) := by
+      nth_rewrite 3 [← inv_simple]
+      have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) :=
+        IsReflection.conj (isReflection_simple cs p) (cs.wordProd l)
+      convert_to
+        IsReflection cs
+          (cs.simple i * (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) *
+            (cs.simple i)⁻¹)
+      · simp[inv_simple, mul_assoc]
+      exact IsReflection.conj this (s i)
+    rw[h (IsReflection.conj (isReflection_simple cs p) (cs.wordProd l))
+      (z + cs.eta i
+        ⟨cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i,
+          this⟩)]
+    rw[permutationMap]
+    apply Prod.ext
+    · simp[conj_of_reflection, mul_assoc]
+    · simp only [eta, add_assoc]
+      by_cases h': cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ = 1
+      · have first_eq :
+            cs.simple i =
+              cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ *
+                cs.simple i := by
+          rw [h']
+          simp
+        rw [if_pos first_eq]
+        have : cs.simple i = cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ := by
+          apply (mul_right_inj (cs.simple i)).mpr at h'
+          simp only[mul_assoc, mul_one] at h'
+          rw[← h']
+          simp[mul_assoc]
+        rw [if_pos this]
+        simp[ZMod]
+        rfl
+      · have first_ne :
+            ¬cs.simple i =
+              cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ *
+                cs.simple i := by
+          intro h''
+          apply h'
+          have hmul := congrArg (fun x => x * cs.simple i) h''
+          simpa [mul_assoc, cs.simple_mul_simple_self] using hmul.symm
+        have second_ne : ¬cs.simple i = cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ := by
+          intro h''
+          apply h'
+          have hmul := congrArg (fun x => cs.simple i * x) h''
+          simpa [mul_assoc, cs.simple_mul_simple_self] using hmul.symm
+        rw [if_neg first_ne, if_neg second_ne]
+        simp
+
+lemma isLeftInversion_iff_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) :
+  cs.IsLeftInversion (cs.wordProd l) t.1 ↔ reflection_mem_leftInvSeq_parity cs l t = 1 := by
+  constructor
+  · intro h
+    by_contra h'
+    have h'' : reflection_mem_leftInvSeq_parity cs l t = 0 := by
+      rw [reflection_mem_leftInvSeq_parity]
+      rw [ZMod.natCast_eq_zero_iff_even]
+      rw[reflection_mem_leftInvSeq_parity] at h'
+      rw[ZMod.natCast_eq_one_iff_odd] at h'
+      exact Nat.not_odd_iff_even.mp h'
+    suffices cs.IsLeftInversion (t.1 * π l) t.1 from by
+      rw[IsLeftInversion] at this
+      rw[← mul_assoc] at this
+      rcases this with ⟨_, ht⟩
+      rw[IsReflection.mul_self t.2] at ht
+      simp at ht
+      simp[IsLeftInversion] at h
+      linarith
+    suffices
+        permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ =
+          ⟨cs.conj_of_reflection t (π l)⁻¹, 1⟩ from by
+      apply isLeftInversion_of_parityReflectionOccurrences_lift_eq_one cs (t.1 * π l) t
+      rw[permutationMap_lift_mk cs (t.1 * π l)⁻¹ t 0] at this
+      simp at this
+      simp[this.2]
+    calc
+      permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ =
+          permutationMap_lift cs (π l)⁻¹ (permutationMap_lift cs t.1 ⟨t, 0⟩) := by
+          simp[IsReflection.inv t.2]
+          rfl
+      _ = permutationMap_lift cs (π l)⁻¹ ⟨t, 1⟩ := by
+          rw[permutationMap_lift_of_reflection cs t 0]
+          simp[permutationMap_lift_mk]
+      _ = ⟨cs.conj_of_reflection t (π l)⁻¹, 1 + parityReflectionOccurrences_lift cs (π l) t⟩ := by
+        simp[permutationMap_lift_mk, conj_of_reflection]
+      _ = (cs.conj_of_reflection t (cs.wordProd l)⁻¹, 1) := by
+        simp
+        simp[parityReflectionOccurrences_lift_mk, h'']
+  · exact isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t
+
+
+theorem strongExchangeProperty (l : List B) (t : cs.Reflection)
+(h' : cs.IsLeftInversion (cs.wordProd l) t.1) :
+  ∃ (k : Fin l.length), t.1 * π l = π (l.eraseIdx k) := by
+  suffices t.1 ∈ cs.leftInvSeq l from eraseIdx_of_mul_leftInvSeq cs l t this
+  rw [isLeftInversion_iff_parityReflectionOccurrences_eq_one cs l t] at h'
+  exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs l t h'
+
+end
+
+end CoxeterSystem
diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml
index 2cd1fd53bb..b9163180c4 100644
--- a/LeanPool/projects.yml
+++ b/LeanPool/projects.yml
@@ -1,4 +1,49 @@
 projects:
+  - slug: demazureoperatorslean
+    title: Demazure Operators and Lean
+    summary: Formalizes Demazure operators on multivariate polynomials and their nilpotence, braid, commutation, and symmetric-polynomial linearity relations, with auxiliary Coxeter-theory support including strong exchange and a conditional Matsumoto theorem.
+    branch: algebraic combinatorics
+    entry_module: LeanPool.DemazureOperatorsLean
+    authors:
+      - Óscar Álvarez Sánchez
+    source:
+      title: "Schubert cells, and the cohomology of the spaces G/P"
+      authors:
+        - I. N. Bernstein
+        - I. M. Gelfand
+        - S. I. Gelfand
+      doi: "10.1070/RM1973v028n03ABEH001549"
+      github_repo: bolito2/DemazureOperatorsLean
+    status: verified
+    main_declarations:
+      - Demazure.Dem
+      - CoxeterSystem.strongExchangeProperty
+    main_results:
+      - declaration: Demazure.Dem
+        informal: Defines the Demazure operator as a linear map over the subalgebra of symmetric polynomials.
+      - declaration: Demazure.demazure_order_two
+        informal: Proves that applying the Demazure operator twice gives zero.
+      - declaration: Demazure.demazure_commutes_adjacent
+        informal: Proves the braid relation for adjacent Demazure operators.
+      - declaration: Demazure.demazure_commutes_non_adjacent
+        informal: Proves that non-adjacent Demazure operators commute.
+      - declaration: Demazure.demazure_mul_symm
+        informal: Proves that symmetric polynomials act as scalars with respect to Demazure operators.
+      - declaration: CoxeterSystem.strongExchangeProperty
+        informal: Proves the strong exchange property for Coxeter systems.
+        source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990."
+      - declaration: CoxeterSystem.matsumoto_reduced
+        informal: Auxiliary theorem proving, under the extra MatsumotoCondition hypothesis, that reduced words for the same Coxeter group element are connected by braid moves.
+        source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990."
+    tags:
+      - algebraic-combinatorics
+      - demazure-operators
+      - polynomials
+      - representation-theory
+    msc:
+      - "05E05"
+      - "13P10"
+      - "20F55"
   - slug: zeta_3_irrational
     title: Beukers integral estimates for ζ(3)
     summary: Formalizes the Beukers integral identities, denominator estimates, positivity, and upper bounds used in Apéry's theorem for ζ(3).