Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-02 21:56 267e6608

View on Github →

refactor(algebra/add_torsor): use to_additive for add_action (#6914)

Estimated changes

deleted theorem vadd_assoc
deleted theorem vadd_comm
deleted theorem vadd_eq_add
deleted theorem vadd_left_cancel
deleted theorem vadd_left_cancel_iff
deleted theorem vadd_left_injective
deleted theorem zero_vadd
deleted theorem prod.smul_fst
deleted theorem prod.smul_mk
deleted theorem prod.smul_snd
modified def const_smul_hom
modified theorem const_smul_hom_apply
modified theorem ite_smul
modified def mul_action.comp_hom
modified def mul_action.to_fun
modified theorem mul_action.to_fun_apply
modified theorem one_smul
modified theorem smul_add
modified theorem smul_comm_class.symm
modified theorem smul_eq_mul
modified theorem smul_ite
modified theorem smul_neg
modified theorem smul_smul
modified theorem smul_sub
modified theorem smul_zero
modified theorem eq_inv_smul_iff
modified theorem inv_smul_eq_iff
modified theorem inv_smul_smul
modified theorem is_unit.smul_left_cancel
modified theorem smul_inv_smul
added theorem smul_left_cancel
added theorem smul_left_cancel_iff
modified theorem units.inv_smul_smul
modified theorem units.smul_inv_smul
modified theorem units.smul_left_cancel
added def units.smul_perm
added theorem prod.smul_fst
added theorem prod.smul_mk
added theorem prod.smul_snd