Theorem CoxeterSystem.exists_isReduced

Modification history

2026-03-29 14:33
Mathlib/GroupTheory/Coxeter/Length.lean
chore(GroupTheory/Coxeter/Length): deprecate redundant theorems (#37155) …
Added CoxeterSystem.exists_isReducedView on Github →