diff --git a/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean b/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean index 47b54b4326bb84..0eada2e8b7a150 100644 --- a/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean +++ b/Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean @@ -38,9 +38,6 @@ variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] open AlgebraicGeometry Manifold TopologicalSpace Topology --- HACK to avoid an instance timeout -attribute [-instance] StarAlgHomClass.toAlgHomClass NonUnitalStarAlgHomClass.toNonUnitalAlgHomClass - /-- The units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered as a sheaf of commutative rings, are the functions whose values at `x` are nonzero. -/ theorem smoothSheafCommRing.isUnit_stalk_iff {x : M}