∀ {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B] (b : B),
  Bundle.Trivialization.coordChangeL 𝕜 (Bundle.Trivial.trivialization B F) (Bundle.Trivial.trivialization B F) b =
    ContinuousLinearEquiv.refl 𝕜 F