Theorem MulAction.contMDiffSMul_compHom

Modification history

2026-05-07 17:04
Mathlib/Geometry/Manifold/Algebra/SMul.lean
feat(Geometry/Manifold): add `ContMDiffSMul` typeclass (#38565) …
Added MulAction.contMDiffSMul_compHomView on Github →