Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-26 10:03 94a228cf

View on Github →

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.

Estimated changes

added theorem of_dual_smul'
deleted theorem of_dual_vadd
modified theorem of_lex_div
modified theorem of_lex_inv
modified theorem of_lex_mul
modified theorem of_lex_pow
added theorem of_lex_smul'
modified theorem of_lex_smul
deleted theorem of_lex_vadd
added theorem pow_of_dual
added theorem pow_of_lex
added theorem pow_to_dual
added theorem pow_to_lex
added theorem to_dual_smul'
deleted theorem to_dual_vadd
added theorem to_lex_smul'
deleted theorem to_lex_vadd