Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-19 12:03 e8858fdd

View on Github →

refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302) Split out mul_opposite from opposite, to leave room for an add_opposite in future. Multiplicative opposites are now spelt Aᵐᵒᵖ instead of Aᵒᵖ. Aᵒᵖ now refers to the categorical opposite.

Estimated changes

modified theorem finset.unop_sum
modified theorem ring_hom.unop_map_list_prod
modified def free_algebra.star_hom
modified def embed_product
added theorem mul_opposite.op_pow
added theorem mul_opposite.op_zpow
added theorem mul_opposite.unop_pow
added theorem mul_opposite.unop_zpow
deleted theorem opposite.op_pow
deleted theorem opposite.op_zpow
deleted theorem opposite.unop_pow
deleted theorem opposite.unop_zpow
modified def mul_equiv.inv'
added def mul_opposite.op
added theorem mul_opposite.op_add
added theorem mul_opposite.op_inj
added theorem mul_opposite.op_inv
added theorem mul_opposite.op_mul
added theorem mul_opposite.op_neg
added theorem mul_opposite.op_one
added theorem mul_opposite.op_smul
added theorem mul_opposite.op_sub
added theorem mul_opposite.op_unop
added theorem mul_opposite.op_zero
added theorem mul_opposite.unop_add
added theorem mul_opposite.unop_inj
added theorem mul_opposite.unop_inv
added theorem mul_opposite.unop_mul
added theorem mul_opposite.unop_neg
added theorem mul_opposite.unop_one
added theorem mul_opposite.unop_op
added theorem mul_opposite.unop_smul
added theorem mul_opposite.unop_sub
added theorem mul_opposite.unop_zero
added def mul_opposite
deleted theorem opposite.coe_op_add_equiv
deleted theorem opposite.commute.op
deleted theorem opposite.commute.unop
deleted theorem opposite.commute_op
deleted theorem opposite.commute_unop
deleted theorem opposite.op_add
deleted theorem opposite.op_eq_one_iff
deleted theorem opposite.op_eq_zero_iff
deleted theorem opposite.op_inv
deleted theorem opposite.op_mul
deleted theorem opposite.op_ne_zero_iff
deleted theorem opposite.op_neg
deleted theorem opposite.op_one
deleted theorem opposite.op_smul
deleted theorem opposite.op_smul_eq_mul
deleted theorem opposite.op_sub
deleted theorem opposite.op_zero
deleted theorem opposite.semiconj_by.op
deleted theorem opposite.semiconj_by.unop
deleted theorem opposite.semiconj_by_op
deleted theorem opposite.semiconj_by_unop
deleted theorem opposite.unop_add
deleted theorem opposite.unop_eq_one_iff
deleted theorem opposite.unop_eq_zero_iff
deleted theorem opposite.unop_inv
deleted theorem opposite.unop_mul
deleted theorem opposite.unop_ne_zero_iff
deleted theorem opposite.unop_neg
deleted theorem opposite.unop_one
deleted theorem opposite.unop_smul
deleted theorem opposite.unop_sub
deleted theorem opposite.unop_zero
modified theorem units.coe_op_equiv_symm
modified theorem units.coe_unop_op_equiv
modified def units.op_equiv
modified theorem quaternion.coe_conj_ae
modified def quaternion.conj_ae
added theorem mul_opposite.op_star
added theorem mul_opposite.unop_star
deleted theorem opposite.op_star
deleted theorem opposite.unop_star
modified def star_mul_equiv
modified def star_ring_equiv
modified theorem category_theory.mop_unmop
modified theorem category_theory.unmop_comp
modified theorem category_theory.unmop_id
modified theorem category_theory.unmop_inj
modified def quiver.hom.mop
modified def quiver.hom.unmop
modified def monoid.foldl
deleted theorem opposite.op_list_prod
deleted theorem opposite.unop_list_prod
added theorem prod.fst_comp_mk
added theorem prod.snd_comp_mk
modified theorem free_product.inv_def
modified structure sesq_form
modified def unique.mk'
modified theorem measurable_op
modified theorem measurable_unop
modified def ring_invo.mk'
modified structure ring_invo
modified theorem continuous_op
modified theorem continuous_unop