Theorem IsLocalFrameOn.mdifferentiableOn_of_coeff

Modification history

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