Mathlib Changelog
v4
Changelog
About
Github
Theorem
Bundle.Trivialization.eq_sum_localFrameCoeff_smul
Modification history
2026-07-27 17:36
Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean
chore(Geometry/Manifold): fix defs with underscores (#42115) …
Added
Bundle.Trivialization.eq_sum_localFrameCoeff_smul
View on Github →