chore(algebra/ne_zero): freeze (#17475)

leanprover-community · Nov 11, 2022 · 4ea7cf6 · 4ea7cf6
1 parent e3968f6
commit 4ea7cf6
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/algebra/ne_zero.lean b/src/algebra/ne_zero.lean
@@ -8,6 +8,10 @@ import logic.basic
 /-!
 # `ne_zero` typeclass
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> https://github.com/leanprover-community/mathlib4/pull/557
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We create a typeclass `ne_zero n` which carries around the fact that `(n : R) ≠ 0`.
 
 ## Main declarations