structure Demazure.PolyFraction' (n : ℕ) : Type

• numerator : MvPolynomial (Fin (n + 1)) ℂ
• denominator : MvPolynomial (Fin (n + 1)) ℂ
• denominator_ne_zero : self.denominator ≠ 0

theorem Demazure.PolyFraction'.denominator_ne_zero {n : ℕ} (self : Demazure.PolyFraction' n) : self.denominator ≠ 0

def Demazure.to_frac {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.PolyFraction' n

Equations

• Demazure.to_frac p = { numerator := p, denominator := 1, denominator_ne_zero := ⋯ }

def Demazure.r (n : ℕ) : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Prop

Equations

• Demazure.r n p q = (p.numerator * q.denominator = q.numerator * p.denominator)

theorem Demazure.r_equiv {n : ℕ} : Equivalence (Demazure.r n)

instance Demazure.s (n : ℕ) : Setoid (Demazure.PolyFraction' n)

Equations

• Demazure.s n = { r := Demazure.r n, iseqv := ⋯ }

instance Demazure.has_equiv {n : ℕ} : HasEquiv (Demazure.PolyFraction' n)

Equations

• Demazure.has_equiv = instHasEquivOfSetoid

theorem Demazure.equiv_r {n : ℕ} {a : Demazure.PolyFraction' n} {b : Demazure.PolyFraction' n} : Demazure.r n a b ↔ a ≈ b

def Demazure.PolyFraction (n : ℕ) : Type

Equations

• Demazure.PolyFraction n = Quotient (Demazure.s n)

def Demazure.mk {n : ℕ} (p : Demazure.PolyFraction' n) : Demazure.PolyFraction n

Equations

• Demazure.mk p = ⟦p⟧

def Demazure.mk' {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.PolyFraction n

Equations

• Demazure.mk' p = Demazure.mk { numerator := p, denominator := 1, denominator_ne_zero := ⋯ }

theorem Demazure.lift_r {n : ℕ} {a : Demazure.PolyFraction' n} {f : Demazure.PolyFraction' n → Demazure.PolyFraction' n} {c : ∀ (a₁ a₂ : Demazure.PolyFraction' n), a₁ ≈ a₂ → (Demazure.mk ∘ f) a₁ = (Demazure.mk ∘ f) a₂} : Quotient.lift (Demazure.mk ∘ f) c (Demazure.mk a) = Demazure.mk (f a)

@[simp]

theorem Demazure.lift2_r {n : ℕ} {a : Demazure.PolyFraction' n} {b : Demazure.PolyFraction' n} {f : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction n} {c : ∀ (a₁ b₁ a₂ b₂ : Demazure.PolyFraction' n), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂} : Quotient.lift₂ f c (Demazure.mk a) (Demazure.mk b) = f a b

@[simp]

theorem Demazure.mk_eq {n : ℕ} {a : Demazure.PolyFraction' n} {b : Demazure.PolyFraction' n} : Demazure.mk a = Demazure.mk b ↔ a.numerator * b.denominator = a.denominator * b.numerator

theorem Demazure.get_polyfraction_rep {n : ℕ} (p : Demazure.PolyFraction n) : ∃ (p' : Demazure.PolyFraction' n), Demazure.mk p' = p

def Demazure.add' {n : ℕ} : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction' n

Equations

• Demazure.add' p q = { numerator := p.numerator * q.denominator + q.numerator * p.denominator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

def Demazure.add_mk {n : ℕ} : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction n

Equations

• Demazure.add_mk p q = Demazure.mk (Demazure.add' p q)

theorem Demazure.add'_s {n : ℕ} (a₁ : Demazure.PolyFraction' n) (b₁ : Demazure.PolyFraction' n) (a₂ : Demazure.PolyFraction' n) (b₂ : Demazure.PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → Demazure.add_mk a₁ b₁ = Demazure.add_mk a₂ b₂

def Demazure.add {n : ℕ} : Demazure.PolyFraction n → Demazure.PolyFraction n → Demazure.PolyFraction n

Equations

• Demazure.add p q = Quotient.lift₂ Demazure.add_mk ⋯ p q

instance Demazure.addition {n : ℕ} : Add (Demazure.PolyFraction n)

Equations

• Demazure.addition = { add := Demazure.add }

instance Demazure.addition' {n : ℕ} : Add (Demazure.PolyFraction' n)

Equations

• Demazure.addition' = { add := Demazure.add' }

def Demazure.sub' {n : ℕ} : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction n

Equations

• Demazure.sub' p q = Demazure.mk { numerator := p.numerator * q.denominator - q.numerator * p.denominator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

theorem Demazure.sub'_s {n : ℕ} (a₁ : Demazure.PolyFraction' n) (b₁ : Demazure.PolyFraction' n) (a₂ : Demazure.PolyFraction' n) (b₂ : Demazure.PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → Demazure.sub' a₁ b₁ = Demazure.sub' a₂ b₂

def Demazure.sub {n : ℕ} : Demazure.PolyFraction n → Demazure.PolyFraction n → Demazure.PolyFraction n

Equations

• Demazure.sub p q = Quotient.lift₂ Demazure.sub' ⋯ p q

def Demazure.mul' {n : ℕ} : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction' n

Equations

• Demazure.mul' p q = { numerator := p.numerator * q.numerator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

def Demazure.mul_mk {n : ℕ} : Demazure.PolyFraction' n → Demazure.PolyFraction' n → Demazure.PolyFraction n

Equations

• Demazure.mul_mk p q = Demazure.mk (Demazure.mul' p q)

theorem Demazure.mul'_s {n : ℕ} (a₁ : Demazure.PolyFraction' n) (b₁ : Demazure.PolyFraction' n) (a₂ : Demazure.PolyFraction' n) (b₂ : Demazure.PolyFraction' n) : a₁ ≈ a₂ → b₁ ≈ b₂ → Demazure.mul_mk a₁ b₁ = Demazure.mul_mk a₂ b₂

def Demazure.mul {n : ℕ} : Demazure.PolyFraction n → Demazure.PolyFraction n → Demazure.PolyFraction n

Equations

• Demazure.mul p q = Quotient.lift₂ Demazure.mul_mk ⋯ p q

instance Demazure.multiplication' {n : ℕ} : Mul (Demazure.PolyFraction' n)

Equations

• Demazure.multiplication' = { mul := Demazure.mul' }

instance Demazure.multiplication {n : ℕ} : Mul (Demazure.PolyFraction n)

Equations

• Demazure.multiplication = { mul := Demazure.mul }

def Demazure.one' {n : ℕ} : Demazure.PolyFraction' n

Equations

• Demazure.one' = { numerator := 1, denominator := 1, denominator_ne_zero := ⋯ }

def Demazure.one {n : ℕ} : Demazure.PolyFraction n

Equations

• Demazure.one = Demazure.mk Demazure.one'

def Demazure.zero' {n : ℕ} : Demazure.PolyFraction' n

Equations

• Demazure.zero' = { numerator := 0, denominator := 1, denominator_ne_zero := ⋯ }

def Demazure.zero {n : ℕ} : Demazure.PolyFraction n

Equations

• Demazure.zero = Demazure.mk Demazure.zero'

def Demazure.neg' {n : ℕ} (p : Demazure.PolyFraction' n) : Demazure.PolyFraction' n

Equations

• Demazure.neg' p = { numerator := -p.numerator, denominator := p.denominator, denominator_ne_zero := ⋯ }

def Demazure.neg_mk {n : ℕ} (p : Demazure.PolyFraction' n) : Demazure.PolyFraction n

Equations

• Demazure.neg_mk p = Demazure.mk (Demazure.neg' p)

theorem Demazure.neg_s (n : ℕ) (a₁ : Demazure.PolyFraction' n) (a₂ : Demazure.PolyFraction' n) : a₁ ≈ a₂ → Demazure.neg_mk a₁ = Demazure.neg_mk a₂

def Demazure.neg {n : ℕ} (p : Demazure.PolyFraction n) : Demazure.PolyFraction n

Equations

• Demazure.neg p = Quotient.lift Demazure.neg_mk ⋯ p

@[simp]

theorem Demazure.add_comm {n : ℕ} (p : Demazure.PolyFraction n) (q : Demazure.PolyFraction n) : Demazure.add p q = Demazure.add q p

@[simp]

theorem Demazure.add_assoc {n : ℕ} (p : Demazure.PolyFraction n) (q : Demazure.PolyFraction n) (r : Demazure.PolyFraction n) : Demazure.add (Demazure.add p q) r = Demazure.add p (Demazure.add q r)

def Demazure.DemAux' {n : ℕ} (i : Fin n) : Demazure.PolyFraction' n → Demazure.PolyFraction' n

Equations

• One or more equations did not get rendered due to their size.

theorem Demazure.DemAux_well_defined {n : ℕ} (i : Fin n) (p : Demazure.PolyFraction' n) (q : Demazure.PolyFraction' n) (h : p ≈ q) : (Demazure.mk ∘ Demazure.DemAux' i) p = (Demazure.mk ∘ Demazure.DemAux' i) q

def Demazure.DemAux {n : ℕ} (i : Fin n) (p : Demazure.PolyFraction n) : Demazure.PolyFraction n

Equations

• Demazure.DemAux i p = Quotient.lift (Demazure.mk ∘ Demazure.DemAux' i) ⋯ p

theorem Demazure.demazure_definitions_equivalent' {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.mk (Demazure.DemAux' i (Demazure.to_frac p)) = Demazure.mk' (Demazure.DemazureFun i p)

theorem Demazure.demazure_definitions_equivalent {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.DemAux i (Demazure.mk' p) = Demazure.mk' (Demazure.DemazureFun i p)

theorem Demazure.eq_zero_of_mk'_zero {n : ℕ} {p : MvPolynomial (Fin (n + 1)) ℂ} : Demazure.mk' p = Demazure.zero ↔ p = 0

theorem Demazure.eq_of_eq_mk' {n : ℕ} {p : MvPolynomial (Fin (n + 1)) ℂ} {q : MvPolynomial (Fin (n + 1)) ℂ} : Demazure.mk' p = Demazure.mk' q ↔ p = q

@[simp]

theorem Demazure.simp_add {n : ℕ} {p : Demazure.PolyFraction n} {q : Demazure.PolyFraction n} : p + q = Demazure.add p q

theorem Demazure.mk_add {n : ℕ} {p : Demazure.PolyFraction' n} {q : Demazure.PolyFraction' n} : Demazure.mk p + Demazure.mk q = Demazure.mk (p + q)

theorem Demazure.mk'_add {n : ℕ} (p : MvPolynomial (Fin (n + 1)) ℂ) (q : MvPolynomial (Fin (n + 1)) ℂ) : Demazure.mk' (p + q) = Demazure.mk' p + Demazure.mk' q

@[simp]

theorem Demazure.simp_mul' {n : ℕ} {p : Demazure.PolyFraction' n} {q : Demazure.PolyFraction' n} : p * q = { numerator := p.numerator * q.numerator, denominator := p.denominator * q.denominator, denominator_ne_zero := ⋯ }

@[simp]

theorem Demazure.simp_mul {n : ℕ} {p : Demazure.PolyFraction n} {q : Demazure.PolyFraction n} : p * q = Demazure.mul p q

theorem Demazure.mk_mul {n : ℕ} {p : Demazure.PolyFraction' n} {q : Demazure.PolyFraction' n} : Demazure.mk p * Demazure.mk q = Demazure.mk (p * q)

theorem Demazure.mk'_mul {n : ℕ} {p : MvPolynomial (Fin (n + 1)) ℂ} {q : MvPolynomial (Fin (n + 1)) ℂ} : Demazure.mk' p * Demazure.mk' q = Demazure.mk' (p * q)