Commit 2023-04-12 19:26 84169f45

View on Github →

chore: forward port mathlib#17611, 18742, 18198, 18520 (#3389) SHA-only updates:

  • leanprover-community/mathlib#17611 – CategoryTheory.Sites.Sheaf already uses aesop_cat at this location, nothing to port.
  • leanprover-community/mathlib#18742 – fiber spelling, which is all of the changes to Topology.FiberBundle.Trivialization, is already in mathlib4.
  • leanprover-community/mathlib#18198 – FunLike change to Data.PEquiv is already in mathlib4. Substantative forward port:
  • leanprover-community/mathlib#18520

Estimated changes