Commit 2024-02-13 12:46 b7c09740

View on Github →

feat(Function): add FactorsThrough.comp_{left,right} (#10449)

Add Function.FactorsThrough.rfl, Function.FactorsThrough.comp_left, and Function.FactorsThrough.comp_right.
Fix a typo in the module docstring of Function/OfArity.

Estimated changes

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.FactorsThrough.comp_left

added theorem Function.FactorsThrough.comp_right

Modified Mathlib/Logic/Function/OfArity.lean