Def RealCopy

Modification history

2025-10-28 09:17

MathlibTest/DifferentialGeometry/NotationAdvanced.lean

feat: further extensions of the differential geometry elaborators (#30413) …

Added RealCopy View on Github →