restore assert_not_exists

leanprover-community · Feb 25, 2025 · c693d12 · c693d12
1 parent 93a5db4
commit c693d12
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Ring/Action/Basic.lean b/Mathlib/Algebra/Ring/Action/Basic.lean
@@ -26,6 +26,8 @@ group action, invariant subring
 
 -/
 
+assert_not_exists Equiv.Perm.equivUnitsEnd Prod.fst_mul
+
 universe u v
 
 /-- Typeclass for multiplicative actions by monoids on semirings.