Update theories/Algebra/Rings/Idempotent.v

Co-authored-by: Dan Christensen <[email protected]>
HoTT · Sep 30, 2024 · 72e906b · 72e906b
1 parent 51ae937
commit 72e906b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v
@@ -42,9 +42,9 @@ Proof.
 Defined.
 
 (** If [e] is idempotent, then it is also an idempotent element of the opposite ring. *)
-Global Instance isidempotent_op (R : Ring) (e : R) `{IsIdempotent R e}
+Global Instance isidempotent_op (R : Ring) (e : R) `{i : IsIdempotent R e}
   : IsIdempotent (rng_op R) e
-  := rng_idem (R:=R).
+  := i.
 
 (** Any positive power of an idempotent element [e] is [e]. *)
 Definition rng_power_idem {R : Ring} (e : R) `{IsIdempotent R e} (n : nat)