Commit 2026-02-27 19:19 f814a024

View on Github →

chore: move a lemma (#31339) This fixes a TODO in that file.

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

deleted theorem Bundle.Trivialization.mdifferentiable

Modified Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

added theorem Bundle.Trivialization.Bundle.Trivialization.mdifferentiable