Theorem TensorialAt.mkHom₂_apply_eq_extend

Modification history

2026-03-10 11:05
Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean
feat(Manifold/VectorBundle): tensoriality construction (#36432) …
Added TensorialAt.mkHom₂_apply_eq_extendView on Github →