theorem CellMulParabolic.bruhatCell_mul_B_right {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : g * b ∈ bp.bruhatCell w

Right $B$-absorption: $C(w) \cdot B \subseteq C(w)$.

theorem CellMulParabolic.bruhatCell_mul_B_left {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hb : b ∈ bp.B) (hg : g ∈ bp.bruhatCell w) : b * g ∈ bp.bruhatCell w

Left $B$-absorption: $B \cdot C(w) \subseteq C(w)$.

theorem CellMulParabolic.cell_mul_simple_in_parabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S' : Set B_idx) (w : M.Group) (s : B_idx) (hs : s ∈ S') (hw : w ∈ bp.parabolicSubgroupW S') (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell w) (hg₂ : g₂ ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)) : ∃ u ∈ ↑(bp.parabolicSubgroupW S'), g₁ * g₂ ∈ bp.bruhatCell u

Single-simple step: if $w \in W_{S'}$ and $s \in S'$, then for $g_1 \in C(w)$ and $g_2 \in C(s)$ the product $g_1 g_2$ lies in some $C(u)$ with $u \in W_{S'}$.

theorem CellMulParabolic.cell_mul_in_parabolic_from_bnpair {G : Type u_3} [Group G] {B_idx : Type u_4} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S' : Set B_idx) (w w' : M.Group) (hw : w ∈ bp.parabolicSubgroupW S') (hw' : w' ∈ bp.parabolicSubgroupW S') (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell w) (hg₂ : g₂ ∈ bp.bruhatCell w') : ∃ u ∈ ↑(bp.parabolicSubgroupW S'), g₁ * g₂ ∈ bp.bruhatCell u

Closure of Bruhat cells under multiplication within a parabolic: if $w, w' \in W_{S'}$ and $g_i \in C(w_i)$, then $g_1 g_2 \in C(u)$ for some $u \in W_{S'}$. This shows $\bigcup_{w \in W_{S'}} C(w) = P_{S'}$ is a subgroup.