We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c154949 commit 2f36b97Copy full SHA for 2f36b97
Mathlib/RingTheory/RingHom/Finite.lean
@@ -25,7 +25,7 @@ theorem finite_stableUnderComposition : StableUnderComposition @Finite := by
25
exact hg.comp hf
26
#align ring_hom.finite_stable_under_composition RingHom.finite_stableUnderComposition
27
28
-instance finite_respectsIso : RespectsIso @Finite := by
+theorem finite_respectsIso : RespectsIso @Finite := by
29
apply finite_stableUnderComposition.respectsIso
30
intros
31
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective
0 commit comments