Theorem mdifferentiable_id
Modification history
2024-10-24 19:28
Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
chore: make the model with corners implicit in differential geometry statements (#17687) …
Modified mdifferentiable_idView on Github →