Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-11-25 11:49
1c3ba7de
View on Github →
lint(geometry/manifold/whitney_embedding): assume
[finite _]
(
#17628
)
Estimated changes
Modified
src/geometry/manifold/whitney_embedding.lean
modified
theorem
smooth_bump_covering.exists_immersion_euclidean