mathlib3
94a228cf - feat(topology/algebra/const_mul_action): `order_dual` instances (#17125)

Commit
3 years ago
feat(topology/algebra/const_mul_action): `order_dual` instances (#17125) A few missing instances for `order_dual`. Namely: * `has_vadd αᵒᵈ β`, `has_smul αᵒᵈ β`, `has_pow αᵒᵈ β` and the corresponding `lex` ones * `has_continuous_const_vadd α βᵒᵈ`, `has_continuous_const_smul α βᵒᵈ` * `has_continuous_const_vadd αᵒᵈ β`, `has_continuous_const_smul αᵒᵈ β` Also fix accidents in `algebra.group.order_synonym`.
Author
Parents
Loading