Commit 2026-04-27 14:17 d848fbac

View on Github →

feat(Logic/Function/Defs): move bicomp from Basic to Defs (#38497)

Estimated changes

Modified Mathlib/Logic/Function/Basic.lean

deleted def Function.bicompl

deleted def Function.bicompr

deleted theorem Function.uncurry_bicompl

deleted theorem Function.uncurry_bicompr

Modified Mathlib/Logic/Function/Defs.lean

added def Function.bicompl

added def Function.bicompr

added theorem Function.uncurry_bicompl

added theorem Function.uncurry_bicompr