Theorem minSmoothness_eq_infty

Modification history

2026-04-17 18:09
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` (#34649) …
Modified minSmoothness_eq_inftyView on Github →
2025-01-19 14:13
Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
feat: start building an API for vector fields on manifolds (#20639) …
Added minSmoothness_eq_inftyView on Github →