We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 905c960 commit 38865c5Copy full SHA for 38865c5
src/Init/Data/Fin/Lemmas.lean
@@ -1139,7 +1139,7 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
1139
theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
1140
| ⟨_, _⟩, ⟨_, _⟩ => rfl
1141
1142
-@[deprecated coe_mul (since := "2025-10-26")]
+@[deprecated val_mul (since := "2025-10-26")]
1143
theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
1144
1145
0 commit comments