Theorem CoxeterSystem.length_le_length_mul_add_left

Modification history

2026-03-25 13:52
Mathlib/GroupTheory/Coxeter/Length.lean
chore(GroupTheory/Coxeter/Length): deprecate nat subtraction lemmas (#37152) …
Added CoxeterSystem.length_le_length_mul_add_leftView on Github →