Theorem IsLocalFrameOn.mdifferentiableAt_of_coeff_aux

Modification history

2025-11-19 10:28
Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean
feat: local frame induced by a vector bundle trivialisation (#31788) …
Modified IsLocalFrameOn.mdifferentiableAt_of_coeff_auxView on Github →
2025-10-23 10:55
Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean
feat: local frames in a vector bundle (#30338) …
Added IsLocalFrameOn.mdifferentiableAt_of_coeff_auxView on Github →