Commit 2024-06-12 09:13 54db0472

View on Github →

chore(Algebra/Order/Module/Defs): remove unused assumptions (#13465)

Estimated changes

Modified Mathlib/Algebra/Order/Module/Defs.lean

modified theorem smul_add_smul_le_smul_add_smul'

modified theorem smul_add_smul_le_smul_add_smul

modified theorem smul_add_smul_lt_smul_add_smul'

modified theorem smul_add_smul_lt_smul_add_smul