Skip to content

Commit 5eed989

Browse files
committed
chore: fix typo intIsManifoldModelSpace (#24297)
Rename `intIsManifoldModelSpace` to `instIsManifoldModelSpace`.
1 parent 085aa9e commit 5eed989

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -690,11 +690,14 @@ theorem isManifold_of_contDiffOn {𝕜 : Type*} [NontriviallyNormedField 𝕜]
690690
alias smoothManifoldWithCorners_of_contDiffOn := isManifold_of_contDiffOn
691691

692692
/-- For any model with corners, the model space is a `C^n` manifold -/
693-
instance intIsManifoldModelSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
693+
instance instIsManifoldModelSpace {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
694694
[NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
695695
{I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} : IsManifold I n H :=
696696
{ hasGroupoid_model_space _ _ with }
697697

698+
@[deprecated (since := "2025-04-22")]
699+
alias intIsManifoldModelSpace := instIsManifoldModelSpace
700+
698701
end IsManifold
699702

700703
namespace IsManifold

0 commit comments

Comments
 (0)