Documentation Verification Report

Hopf_

📁 Source: Mathlib/CategoryTheory/Monoidal/Hopf_.lean

Statistics

Metric	Count
Definitions `Hopf`, `X`, `hopf`, `instCategory`, `toBimon`, `toBimon_`, `HopfObj`, `antipode`, `term𝒮`, `toBimonObj`, `«term𝒮[_]»`, `Hopf_`, `Hopf_Class`	13
Theorems `antipode_antipode`, `antipode_comul`, `antipode_comul₁`, `antipode_comul₂`, `antipode_counit`, `antipode_counit_assoc`, `antipode_left`, `antipode_left_assoc`, `antipode_right`, `antipode_right_assoc`, `hom_antipode`, `mul_antipode`, `mul_antipode₁`, `mul_antipode₂`, `one_antipode`, `one_antipode_assoc`	16
Total	29

CategoryTheory

Definitions

Name	Category	Theorems
`Hopf` 📖	CompData	—
`HopfObj` 📖	CompData	—
`Hopf_` 📖	CompOp	—
`Hopf_Class` 📖	CompOp	—

CategoryTheory.Hopf

Definitions

Name	Category	Theorems
`X` 📖	CompOp	—
`hopf` 📖	CompOp	—
`instCategory` 📖	CompOp	—
`toBimon` 📖	CompOp	—
`toBimon_` 📖	CompOp	—

CategoryTheory.HopfObj

Definitions

Name	Category	Theorems
`antipode` 📖	CompOp	16 math math: `mul_antipode`, `one_antipode`, `antipode_left`, `antipode_comul`, `antipode_comul₂`, `antipode_left_assoc`, `mul_antipode₁`, `antipode_right_assoc`, `antipode_comul₁`, `antipode_antipode`, `mul_antipode₂`, `antipode_counit`, `antipode_right`, `antipode_counit_assoc`, `one_antipode_assoc`, `hom_antipode`
`term𝒮` 📖	CompOp	—
`toBimonObj` 📖	CompOp	14 math math: `mul_antipode`, `one_antipode`, `antipode_left`, `antipode_comul`, `antipode_comul₂`, `antipode_left_assoc`, `mul_antipode₁`, `antipode_right_assoc`, `antipode_comul₁`, `mul_antipode₂`, `antipode_counit`, `antipode_right`, `antipode_counit_assoc`, `one_antipode_assoc`
`«term𝒮[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antipode_antipode` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `toBimonObj`	`antipode` `CategoryTheory.CategoryStruct.id`	—	`left_inv_eq_right_inv` `CategoryTheory.Conv.mul_eq` `CategoryTheory.Conv.one_eq` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.tensorHom_def_assoc` `mul_antipode` `antipode_left_assoc` `one_antipode` `CategoryTheory.MonoidalCategory.whiskerLeft_id` `CategoryTheory.Category.id_comp` `antipode_left`
`antipode_comul` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `antipode` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`left_inv_eq_right_inv` `CategoryTheory.Conv.mul_eq` `CategoryTheory.Conv.one_eq` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.MonoidalCategory.tensor_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `antipode_comul₁` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `antipode_comul₂`
`antipode_comul₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `antipode` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.associator_naturality_right` `CategoryTheory.MonoidalCategory.tensorHom_def` `CategoryTheory.Bimon.compatibility` `antipode_left` `CategoryTheory.BimonObj.one_comul`
`antipode_comul₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `antipode` `CategoryTheory.Iso.inv` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.tensorHom_def'` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `CategoryTheory.MonoidalCategory.associator_inv_naturality_middle` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.BraidedCategory.braiding_naturality_right` `CategoryTheory.MonoidalCategory.associator_naturality_left` `CategoryTheory.BraidedCategory.braiding_naturality_left` `CategoryTheory.MonoidalCategory.associator_inv_naturality_right` `CategoryTheory.MonoidalCategory.whisker_exchange` `CategoryTheory.BraidedCategory.hexagon_reverse_assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.ComonObj.comul_assoc_flip_assoc` `CategoryTheory.ComonObj.comul_assoc` `CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `antipode_right` `CategoryTheory.ComonObj.counit_comul` `CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc` `CategoryTheory.braiding_tensorUnit_left` `CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv` `CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor` `CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc` `antipode_right_assoc` `CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc` `CategoryTheory.MonoidalCategory.tensorHom_def` `Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Monoidal.eval_comp` `Mathlib.Tactic.Monoidal.eval_of` `Mathlib.Tactic.Monoidal.eval_whiskerRight` `Mathlib.Tactic.Monoidal.evalWhiskerRight_id` `Mathlib.Tactic.Monoidal.evalComp_cons` `Mathlib.Tactic.Monoidal.evalComp_nil_nil` `Mathlib.Tactic.Monoidal.evalComp_nil_cons` `Mathlib.Tactic.Monoidal.eval_whiskerLeft` `Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Monoidal.mk_eq_of_naturality` `Mathlib.Tactic.Monoidal.naturality_id` `Mathlib.Tactic.Monoidal.naturality_comp` `Mathlib.Tactic.Monoidal.naturality_inv` `Mathlib.Tactic.Monoidal.naturality_rightUnitor` `Mathlib.Tactic.Monoidal.naturality_leftUnitor` `Mathlib.Tactic.Monoidal.naturality_whiskerLeft`
`antipode_counit` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `antipode` `CategoryTheory.ComonObj.counit` `CategoryTheory.BimonObj.toComonObj` `toBimonObj`	—	`CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.MonoidalCategory.unitors_equal` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.ComonObj.comul_counit_assoc` `CategoryTheory.BimonObj.one_counit` `CategoryTheory.MonoidalCategory.whisker_exchange_assoc` `CategoryTheory.MonoidalCategory.tensorHom_def'` `CategoryTheory.Bimon.mul_counit` `antipode_left_assoc`
`antipode_counit_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `antipode` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.counit` `CategoryTheory.BimonObj.toComonObj` `toBimonObj`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `antipode_counit`
`antipode_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `antipode` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonObj.one`	—	—
`antipode_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `antipode` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `antipode_left`
`antipode_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `antipode` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonObj.one`	—	—
`antipode_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `antipode` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `antipode_right`
`hom_antipode` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `antipode`	—	`left_inv_eq_right_inv` `CategoryTheory.Conv.mul_eq` `CategoryTheory.Conv.one_eq` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.whisker_exchange` `CategoryTheory.MonoidalCategory.tensorHom_def` `CategoryTheory.IsComonHom.hom_comul` `CategoryTheory.IsBimonHom.toIsComonHom` `antipode_left` `CategoryTheory.IsComonHom.hom_counit` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `CategoryTheory.IsMonHom.mul_hom` `CategoryTheory.IsBimonHom.toIsMonHom` `antipode_right` `CategoryTheory.IsMonHom.one_hom`
`mul_antipode` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `toBimonObj` `antipode` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding`	—	`left_inv_eq_right_inv` `CategoryTheory.Conv.mul_eq` `CategoryTheory.Conv.one_eq` `CategoryTheory.Comon.tensorObj_comul` `CategoryTheory.MonoidalCategory.whiskerRight_tensor` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc` `mul_antipode₁` `CategoryTheory.BraidedCategory.braiding_naturality_assoc` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `mul_antipode₂`
`mul_antipode₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `antipode` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.associator_naturality_left` `CategoryTheory.MonoidalCategory.whisker_exchange` `CategoryTheory.MonoidalCategory.tensorHom_def` `CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc` `CategoryTheory.Bimon.compatibility_assoc` `antipode_left` `CategoryTheory.BimonObj.mul_counit_assoc`
`mul_antipode₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.ComonObj.comul` `CategoryTheory.BimonObj.toComonObj` `toBimonObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.MonObj.mul` `CategoryTheory.BimonObj.toMonObj` `antipode` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.ComonObj.counit` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonObj.one`	—	`CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.associator_naturality_left` `CategoryTheory.MonoidalCategory.whisker_exchange` `CategoryTheory.MonObj.mul_assoc_flip` `CategoryTheory.MonoidalCategory.associator_inv_naturality_left` `CategoryTheory.MonObj.mul_assoc` `CategoryTheory.MonoidalCategory.comp_whiskerRight` `CategoryTheory.MonoidalCategory.tensorHom_def` `CategoryTheory.MonoidalCategory.tensor_whiskerLeft` `CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.id_comp` `CategoryTheory.BraidedCategory.hexagon_forward` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv` `CategoryTheory.MonoidalCategory.whisker_assoc` `CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc` `CategoryTheory.BraidedCategory.braiding_naturality_right` `CategoryTheory.MonoidalCategory.tensorHom_def'` `CategoryTheory.MonoidalCategory.associator_naturality_right` `CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `antipode_right` `CategoryTheory.MonObj.one_mul` `CategoryTheory.BraidedCategory.braiding_naturality_left` `CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc` `CategoryTheory.braiding_tensorUnit_right` `CategoryTheory.MonoidalCategory.whiskerLeft_id` `CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor` `CategoryTheory.MonoidalCategory.rightUnitor_naturality` `CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc` `Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Monoidal.eval_comp` `Mathlib.Tactic.Monoidal.eval_tensorHom` `Mathlib.Tactic.Monoidal.eval_of` `Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons` `Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of` `Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil` `Mathlib.Tactic.Monoidal.evalComp_cons` `Mathlib.Tactic.Monoidal.evalComp_nil_nil` `Mathlib.Tactic.Monoidal.evalComp_nil_cons` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Monoidal.mk_eq_of_naturality` `Mathlib.Tactic.Monoidal.naturality_comp` `Mathlib.Tactic.Monoidal.naturality_tensorHom` `Mathlib.Tactic.Monoidal.naturality_id` `Mathlib.Tactic.Monoidal.naturality_rightUnitor` `Mathlib.Tactic.Monoidal.naturality_leftUnitor`
`one_antipode` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonObj.one` `CategoryTheory.BimonObj.toMonObj` `toBimonObj` `antipode`	—	`CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.MonObj.mul_one` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.BimonObj.one_counit_assoc` `CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc` `CategoryTheory.MonoidalCategory.whisker_exchange_assoc` `CategoryTheory.MonoidalCategory.unitors_inv_equal` `CategoryTheory.MonoidalCategory.tensorHom_def_assoc` `CategoryTheory.Bimon.one_comul_assoc` `antipode_left`
`one_antipode_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonObj.one` `CategoryTheory.BimonObj.toMonObj` `toBimonObj` `antipode`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `one_antipode`

---

← Back to Index