Mathlib v3 is deprecated. Go to Mathlib v4

Theorem of_lex_smul'

Modification history

2022-10-26 10:03
src/algebra/group/order_synonym.lean
feat(topology/algebra/const_mul_action): `order_dual` instances (#17125) …
Added of_lex_smul'View on Github →