Commit 2026-03-29 14:33 7984739c
View on Github →chore(GroupTheory/Coxeter/Length): deprecate redundant theorems (#37155)
We deprecate exists_reduced_word and exists_reduced_word' in favor of a common exists_isReduced, which we accomplish by moving the definition IsReduced earlier in the file.