Theorem inTangentCoordinates_eq_mfderiv_comp_abuse

Modification history

2026-08-20 12:42
Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
chore: fix defeq abuse in the definition of MFDeriv (#42193) …
Added inTangentCoordinates_eq_mfderiv_comp_abuseView on Github →