Theorem writtenInExtChart_prod

Modification history

2026-02-19 09:41
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
chore(Geometry/Manifold): rename `writtenInExtChart_prod` to `writtenInExtChartAt_prod` (#35511) …
Deleted writtenInExtChart_prodView on Github →
2025-10-29 00:03
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
feat: add mfderiv_prod and mfderiv_prodMap (#29589) …
Added writtenInExtChart_prodView on Github →