Planar rooks algebras as a cellular algebra

theorem SModEq.refl' {R : Type u_1} [Ring R] {M : Type u_4} [AddCommGroup M] [Module R M] {U : Submodule R M} (x y : M) (h : x = y) : x ≡ y [SMOD U]

noncomputable def my_r (k : Type) [Field k] (δ : k) (n : ℕ) : (ν : Fin (n + 1)) × { S : Finset (Fin n) // S.card = ↑ν } × { S : Finset (Fin n) // S.card = ↑ν } → (μ : Fin (n + 1)) → { S : Finset (Fin n) // S.card = ↑μ } → { S : Finset (Fin n) // S.card = ↑μ } → k

Equations

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

noncomputable instance instCellularAlgebraAlgebra (k : Type) [Field k] (δ : k) [DecidableEq k] (n : ℕ) : CellularAlgebra k (PlanarRook.Algebra n δ)

Equations

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