Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-22 17:15 8bab60f0

View on Github →

fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679)

  • Also add a simps attribute on one construction.

Estimated changes