Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-14 12:02
87adde49
View on Github →
feat(category_theory/monoidal): the monoidal opposite (
#7602
)
Estimated changes
Created
src/category_theory/monoidal/opposite.lean
added
def
category_theory.iso.mop
added
def
category_theory.monoidal_opposite.mop
added
theorem
category_theory.monoidal_opposite.mop_unmop
added
theorem
category_theory.monoidal_opposite.op_inj_iff
added
theorem
category_theory.monoidal_opposite.op_injective
added
def
category_theory.monoidal_opposite.unmop
added
theorem
category_theory.monoidal_opposite.unmop_mop
added
theorem
category_theory.monoidal_opposite.unop_inj_iff
added
theorem
category_theory.monoidal_opposite.unop_injective
added
def
category_theory.monoidal_opposite
added
theorem
category_theory.mop_comp
added
theorem
category_theory.mop_id
added
theorem
category_theory.mop_id_unmop
added
theorem
category_theory.mop_inj
added
theorem
category_theory.mop_tensor_obj
added
theorem
category_theory.mop_tensor_unit
added
theorem
category_theory.mop_unmop
added
theorem
category_theory.op_tensor_obj
added
theorem
category_theory.op_tensor_unit
added
theorem
category_theory.unmop_comp
added
theorem
category_theory.unmop_id
added
theorem
category_theory.unmop_id_mop
added
theorem
category_theory.unmop_inj
added
theorem
category_theory.unmop_mop
added
def
quiver.hom.mop
added
def
quiver.hom.unmop