Theorem abs_smul

Modification history

2025-08-27 16:04
Mathlib/Algebra/Order/Module/Basic.lean
chore(Algebra/Order): move `x ⊓ y = (⅟2 : α) • (x + y - |y - x|)` (#28900) …
Modified abs_smulView on Github →
2025-06-24 23:05
Mathlib/Algebra/Order/Module/Basic.lean
feat(Algebra/Order): more general version of `abs_qsmul` (#26179) …
Added abs_smulView on Github →