mathlib
8bab60f0 - fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679)

Commit
3 years ago
fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679) * Also add a `simps` attribute on one construction.
Author
Parents
Loading