feat(Geometry/Manifold/VectorBundle/Tangent): tangentCoordChange (#8672) #5954
Annotations
3 errors
|
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean#L161
unknown identifier 'LocalEquiv.trans_source'''
|
|
Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean#L161
tactic 'rewrite' failed, equality or iff proof expected
|
|
|
The logs for this run have expired and are no longer available.
Loading