Theorem contMDiff_finset_prod'

Modification history

2026-03-05 11:23
Mathlib/Geometry/Manifold/Algebra/Monoid.lean
chore(Geometry/Manifold/Algebra): golf using custom elaborators (#36007)
Modified contMDiff_finset_prod'View on Github →
2023-06-24 15:15
Mathlib/Geometry/Manifold/Algebra/Monoid.lean
feat: port Geometry.Manifold.Algebra.Monoid (#5438)
Added contMDiff_finset_prod'View on Github →