From adcec8e67aa0fe6246ac8a06563654711e73d34e Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Thu, 8 Feb 2024 00:09:02 -0800
Subject: [PATCH] chore: upstream Divides class and syntax (#3283)

This just upstreams the class and notation. Instances will be provided
with Nat/Int upstream
---
 src/Init/Notation.lean | 1 +
 src/Init/Prelude.lean  | 5 +++++
 2 files changed, 6 insertions(+)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index e74a543faf..08ba15eec8 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -268,6 +268,7 @@ syntax (name := rawNatLit) "nat_lit " num : term
 @[inherit_doc] infixr:90 " ∘ "  => Function.comp
 @[inherit_doc] infixr:35 " × "  => Prod
 
+@[inherit_doc] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr
 @[inherit_doc] infixl:58 " ^^^ " => HXor.hXor
 @[inherit_doc] infixl:60 " &&& " => HAnd.hAnd
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index db2b91608a..5d5a73e2cc 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1314,6 +1314,11 @@ class Mod (α : Type u) where
   /-- `a % b` computes the remainder upon dividing `a` by `b`. See `HMod`. -/
   mod : α → α → α
 
+/-- Notation typeclass for the `∣` operation (typed as `\|`), which represents divisibility. -/
+class Dvd (α : Type _) where
+  /-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. -/
+  dvd : α → α → Prop
+
 /--
 The homogeneous version of `HPow`: `a ^ b : α` where `a : α`, `b : β`.
 (The right argument is not the same as the left since we often want this even