Commit 2024-07-16 07:40 f0587c5d

View on Github →

chore(Logic/Function/Defs): move file out of Init (#14754)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Control/Traversable/Basic.lean

Modified Mathlib/Data/Bool/Basic.lean

Modified Mathlib/Data/List/Defs.lean

Modified Mathlib/Data/Option/NAry.lean

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Prod/PProd.lean

Modified Mathlib/Data/Sigma/Basic.lean

Modified Mathlib/Logic/Basic.lean

modified theorem Imp.swap

deleted theorem PLift.down_inj

deleted theorem PLift.down_injective

deleted theorem ULift.down_inj

deleted theorem ULift.down_injective

modified theorem forall_swap

Modified Mathlib/Logic/Function/CompTypeclasses.lean

Renamed Mathlib/Init/Function.lean to Mathlib/Logic/Function/Defs.lean

Created Mathlib/Logic/Function/ULift.lean

added theorem PLift.down_inj

added theorem PLift.down_injective

added theorem ULift.down_inj

added theorem ULift.down_injective

Modified Mathlib/Logic/Nonempty.lean

Modified Mathlib/Logic/Nontrivial/Defs.lean

Modified Mathlib/Logic/Relator.lean

Modified Mathlib/Order/ULift.lean

Modified Mathlib/Tactic/DeriveTraversable.lean

Modified scripts/noshake.json

Modified test/apply_fun.lean