chore(logic/function/basic): make function.injective.decidable_eq p…

…rotected (#15759)
leanprover-community · Jul 30, 2022 · a574fbe · a574fbe
1 parent 348a674
commit a574fbe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean
@@ -86,7 +86,7 @@ h ▸ hf.ne_iff
 
 /-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
 the domain `α` also has decidable equality. -/
-def injective.decidable_eq [decidable_eq β] (I : injective f) : decidable_eq α :=
+protected def injective.decidable_eq [decidable_eq β] (I : injective f) : decidable_eq α :=
 λ a b, decidable_of_iff _ I.eq_iff
 
 lemma injective.of_comp {g : γ → α} (I : injective (f ∘ g)) : injective g :=