Commit 2024-11-13 08:11 8ee2f8b8

View on Github →

chore: camel sectl and sectr (#18907) ... to sectL and sectR. I personally find these names much less confusing this way.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

Modified Mathlib/CategoryTheory/ChosenFiniteProducts/Cat.lean

modified theorem CategoryTheory.Monoidal.leftUnitor_inv

modified theorem CategoryTheory.Monoidal.rightUnitor_inv

Modified Mathlib/CategoryTheory/Limits/IndYoneda.lean

Modified Mathlib/CategoryTheory/Products/Basic.lean

added def CategoryTheory.Prod.sectL

added def CategoryTheory.Prod.sectR

deleted def CategoryTheory.Prod.sectl

deleted def CategoryTheory.Prod.sectr

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/Logic/Embedding/Basic.lean

added def Function.Embedding.sectL

added def Function.Embedding.sectR

deleted def Function.Embedding.sectl

deleted def Function.Embedding.sectr