Def tangentSpaceCast

Modification history

2026-08-20 12:42

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

chore: fix defeq abuse in the definition of MFDeriv (#42193) …

Added tangentSpaceCast View on Github →