Commit 2026-03-25 10:07 9995f19d
View on Github →chore(GroupTheory/Coxeter/Length): remove backward.privateInPublic (#37150)
We don't need to expose the definition of length, as it's characterized entirely by exists_reduced_word and length_wordProd_le.