Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 13:36 aa82ba00

View on Github →

feat(algebra/opposites): add add_opposite (#11080) Add add_opposite, add to_additive here and there. More to_additive can be added as needed later.

Estimated changes

added def add_equiv.mul_op
deleted def add_equiv.op
deleted def add_equiv.unop
deleted def add_monoid_hom.op
deleted theorem add_monoid_hom.op_ext
deleted def add_monoid_hom.unop
added theorem add_opposite.op_pow
added theorem add_opposite.unop_pow
added theorem commute.op
modified def monoid_hom.op
modified def monoid_hom.unop
modified def mul_equiv.unop
deleted theorem mul_opposite.commute.op
modified theorem mul_opposite.commute.unop
modified theorem mul_opposite.commute_op
modified theorem mul_opposite.commute_unop
modified theorem mul_opposite.semiconj_by_op
added theorem semiconj_by.op
added theorem semiconj_by.unop
modified theorem units.coe_op_equiv_symm
modified theorem units.coe_unop_op_equiv
modified def units.op_equiv
added theorem add_opposite.op_div
added theorem add_opposite.op_inv
added theorem add_opposite.op_mul
added theorem add_opposite.op_one
added theorem add_opposite.unop_div
added theorem add_opposite.unop_inv
added theorem add_opposite.unop_mul
added theorem add_opposite.unop_one
modified theorem mul_opposite.op_bijective
modified theorem mul_opposite.op_comp_unop
modified theorem mul_opposite.op_eq_one_iff
modified theorem mul_opposite.op_eq_zero_iff
modified theorem mul_opposite.op_inj
modified theorem mul_opposite.op_injective
modified theorem mul_opposite.op_inv
modified theorem mul_opposite.op_mul
modified theorem mul_opposite.op_ne_zero_iff
modified theorem mul_opposite.op_one
modified theorem mul_opposite.op_smul
modified theorem mul_opposite.op_surjective
modified theorem mul_opposite.op_unop
modified theorem mul_opposite.unop_bijective
modified theorem mul_opposite.unop_comp_op
modified theorem mul_opposite.unop_inj
modified theorem mul_opposite.unop_injective
modified theorem mul_opposite.unop_inv
modified theorem mul_opposite.unop_mul
modified theorem mul_opposite.unop_one
modified theorem mul_opposite.unop_op
modified theorem mul_opposite.unop_smul
modified theorem op_smul_eq_mul