@[deprecated "Use exchange_implies_deletion_unconditional from UnconditionalExchange.lean" (since := "2025-01-01")]
theorem
CoxeterExchange.exchange_implies_deletion
{B : Type u_1}
[DecidableEq B]
[Fintype B]
{W : Type u_2}
[Group W]
{M : CoxeterMatrix B}
(cs : CoxeterSystem M W)
(hsce : SignChangeExchangeHyp M cs)
:
Deprecated wrapper deriving the deletion condition from the sign-change exchange hypothesis (use the unconditional version instead).
@[deprecated "Use exchange_implies_corollary_unconditional from UnconditionalExchange.lean" (since := "2025-01-01")]
theorem
CoxeterExchange.exchange_implies_corollary
{B : Type u_1}
[DecidableEq B]
[Fintype B]
{W : Type u_2}
[Group W]
{M : CoxeterMatrix B}
(cs : CoxeterSystem M W)
(hsce : SignChangeExchangeHyp M cs)
:
ExchangeCorollary M cs
Deprecated wrapper deriving the exchange corollary from the sign-change exchange hypothesis (use the unconditional version instead).
@[deprecated "Use exchange_implies_both_unconditional from UnconditionalExchange.lean" (since := "2025-01-01")]
theorem
CoxeterExchange.exchange_implies_both
{B : Type u_1}
[DecidableEq B]
[Fintype B]
{W : Type u_2}
[Group W]
{M : CoxeterMatrix B}
(cs : CoxeterSystem M W)
(hsce : SignChangeExchangeHyp M cs)
:
Deprecated combined wrapper: the sign-change exchange hypothesis implies both the deletion condition and the exchange corollary.