Mathlib v3 is deprecated. Go to Mathlib v4

Def ordered_semimodule.mk'

Modification history

2020-10-30 08:20
src/algebra/module/ordered.lean
refactor(module/ordered): make ordered_semimodule a mixin (#4719) …
Deleted ordered_semimodule.mk'View on Github →
2020-10-20 08:10
src/algebra/module/ordered.lean
feat(linear_algebra/affine_space/ordered): define `slope` (#4669) …
Added ordered_semimodule.mk'View on Github →