Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-21 09:59 e0b2fa6d

View on Github →

feat(algebra/*): Algebraic instances on lex/order_dual (#16122) Copy over algebraic instances for lex and order_dual.

Estimated changes

added theorem of_dual_rat_cast
added theorem of_lex_rat_cast
added theorem to_dual_rat_cast
added theorem to_lex_rat_cast
added theorem of_dual_div
added theorem of_dual_inv
added theorem of_dual_mul
added theorem of_dual_one
added theorem of_dual_pow
added theorem of_dual_smul
added theorem of_dual_vadd
added theorem of_lex_div
added theorem of_lex_inv
added theorem of_lex_mul
added theorem of_lex_one
added theorem of_lex_pow
added theorem of_lex_smul
added theorem of_lex_vadd
added theorem to_dual_div
added theorem to_dual_inv
added theorem to_dual_mul
added theorem to_dual_one
added theorem to_dual_pow
added theorem to_dual_smul
added theorem to_dual_vadd
added theorem to_lex_div
added theorem to_lex_inv
added theorem to_lex_mul
added theorem to_lex_one
added theorem to_lex_pow
added theorem to_lex_smul
added theorem to_lex_vadd
deleted theorem order_dual.of_dual_smul
deleted theorem order_dual.to_dual_smul
added theorem of_dual_int_cast
added theorem of_lex_int_cast
added theorem to_dual_int_cast
added theorem to_lex_int_cast
added theorem of_dual_nat_cast
added theorem of_lex_nat_cast
modified theorem pi.coe_nat
modified theorem pi.nat_apply
added theorem to_dual_nat_cast
added theorem to_lex_nat_cast
modified structure decorated_equiv
added def equiv'.trans
added structure equiv'
deleted def equiv.trans
deleted structure equiv
modified def foo2
modified def my_equiv