Theorem CoxeterSystem.length_wordProd_le

Modification history

2026-07-08 09:06
Mathlib/GroupTheory/Coxeter/Length.lean
chore: remove redundant `open scoped Classical` (#41423) …
Modified CoxeterSystem.length_wordProd_leView on Github →
2024-05-11 18:18
Mathlib/GroupTheory/Coxeter/Length.lean
feat: length, reduced words in Coxeter groups (#11465) …
Added CoxeterSystem.length_wordProd_leView on Github →