Commit 2025-06-27 10:00 8bb6112a

View on Github →

chore(CategoryTheory/Monoidal): fix a few lemma names (#26256) Some were missing a trailing _hom, some had the _inv misplaced.

Estimated changes

Modified Mathlib/CategoryTheory/Enriched/Opposite.lean

Modified Mathlib/CategoryTheory/GradedObject/Braiding.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

deleted theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_left

deleted theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_right

deleted theorem CategoryTheory.BraidedCategory.braiding_tensor_left

added theorem CategoryTheory.BraidedCategory.braiding_tensor_left_hom

added theorem CategoryTheory.BraidedCategory.braiding_tensor_left_inv

deleted theorem CategoryTheory.BraidedCategory.braiding_tensor_right

added theorem CategoryTheory.BraidedCategory.braiding_tensor_right_hom

added theorem CategoryTheory.BraidedCategory.braiding_tensor_right_inv

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom

deleted theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor

added theorem CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom

Modified Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor''

deleted theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom''

added theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean

Modified scripts/nolints_prime_decls.txt