Commit 2026-03-25 13:52 d2918370

View on Github →

chore(GroupTheory/Coxeter/Length): deprecate nat subtraction lemmas (#37152) In favor of equivalent theorems expressed with addition.

Estimated changes

Modified Mathlib/GroupTheory/Coxeter/Length.lean

added theorem CoxeterSystem.length_le_length_mul_add_left

added theorem CoxeterSystem.length_le_length_mul_add_right

modified theorem CoxeterSystem.length_mul_ge_length_sub_length'

modified theorem CoxeterSystem.length_mul_ge_length_sub_length

modified theorem CoxeterSystem.length_mul_ge_max

modified theorem CoxeterSystem.length_mul_le

modified theorem CoxeterSystem.length_mul_simple

modified theorem CoxeterSystem.length_simple_mul