chore: deprecate Ordinal.one_ne_zero → _root_.one_ne_zero

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -813,7 +813,7 @@ theorem div_eq_one_iff {a b : Ordinal} : a / b = 1 ↔ b ≤ a ∧ a < b * 2 :=
 
 @[simp]
 theorem div_one (a : Ordinal) : a / 1 = a := by
-  simpa only [one_mul] using mul_div_cancel a Ordinal.one_ne_zero
+  simpa only [one_mul] using mul_div_cancel a one_ne_zero
 
 @[simp]
 theorem div_self {a : Ordinal} (h : a ≠ 0) : a / a = 1 := by

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -219,11 +219,15 @@ theorem nonempty_toType_iff {o : Ordinal} : Nonempty o.ToType ↔ o ≠ 0 := by
 
 @[deprecated (since := "2026-02-18")] alias toType_nonempty_iff_ne_zero := nonempty_toType_iff
 
+instance instNeZeroOne : NeZero (1 : Ordinal) :=
+  ⟨type_ne_zero_of_nonempty _⟩
+
+@[deprecated _root_.one_ne_zero (since := "2026-05-12")]
 protected theorem one_ne_zero : (1 : Ordinal) ≠ 0 :=
-  type_ne_zero_of_nonempty _
+  _root_.one_ne_zero
 
 instance nontrivial : Nontrivial Ordinal.{u} :=
-  ⟨⟨1, 0, Ordinal.one_ne_zero⟩⟩
+  ⟨⟨1, 0, one_ne_zero⟩⟩
 
 /-- `Quotient.inductionOn` specialized to ordinals.
 
@@ -354,9 +358,6 @@ protected theorem not_lt_zero (o : Ordinal) : ¬o < 0 :=
 @[deprecated eq_zero_or_pos (since := "2025-11-21")]
 protected theorem eq_zero_or_pos : ∀ a : Ordinal, a = 0 ∨ 0 < a := eq_bot_or_bot_lt
 
-instance instNeZeroOne : NeZero (1 : Ordinal) :=
-  ⟨Ordinal.one_ne_zero⟩
-
 theorem type_le_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r]
     [IsWellOrder β s] : type r ≤ type s ↔ Nonempty (r ≼i s) :=
   Iff.rfl

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -91,7 +91,7 @@ theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by
     simp only [opow_succ, ih, mul_one]
   | limit b l IH =>
     refine eq_of_forall_ge_iff fun c => ?_
-    rw [opow_le_of_isSuccLimit Ordinal.one_ne_zero l]
+    rw [opow_le_of_isSuccLimit one_ne_zero l]
     exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
 
 theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by
@@ -198,7 +198,7 @@ theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := b
   rcases le_or_gt a 1 with a1 | a1
   · rcases lt_or_eq_of_le a1 with a0 | a1
     · rw [lt_one_iff] at a0
-      rw [a0, zero_opow Ordinal.one_ne_zero]
+      rw [a0, zero_opow one_ne_zero]
       exact zero_le
     rw [a1, one_opow, one_opow]
   rwa [opow_le_opow_iff_right a1, one_le_iff_pos]