Separate div2_zero out from Div2, to allow types that don't have a Zero

Author: girving

Interval/Approx/Div2.lean

@@ -16,15 +16,19 @@ variable {α 𝕜 : Type}
 section Defs
 
 /-- Division by 2 -/
-class Div2 α [Zero α] where
+class Div2 α where
   div2 : α → α
-  div2_zero : div2 (0 : α) = 0
 
-export Div2 (div2 div2_zero)
+/-- Division by 2 respects zero -/
+class Div2Zero α [Zero α] [Div2 α] where
+  div2_zero : Div2.div2 (0 : α) = 0
+
+export Div2 (div2)
+export Div2Zero (div2_zero)
 attribute [simp] div2_zero
 
 /-- Division by 2 is conservative -/
-class ApproxDiv2 (α α' : Type) [Approx α α'] [Zero α] [Zero α'] [Div2 α] [Div2 α'] where
+class ApproxDiv2 (α α' : Type) [Approx α α'] [Div2 α] [Div2 α'] where
   approx_div2 {x : α} {x' : α'} (a : approx x x') : approx (div2 x) (div2 x')
 
 export ApproxDiv2 (approx_div2)
@@ -45,6 +49,9 @@ variable {E : Type} [Zero E] [SMulZeroClass ℚ E]
 /-- Division by 2 for modules -/
 instance {E : Type} [Zero E] [SMulZeroClass ℚ E] : Div2 E where
   div2 x := (2⁻¹ : ℚ) • x
+
+/-- Division by 2 respects zero for modules -/
+instance {E : Type} [Zero E] [SMulZeroClass ℚ E] : Div2Zero E where
   div2_zero := smul_zero _
 
 lemma div2_eq_smul {E : Type} [Zero E] [SMulZeroClass ℚ E] (x : E) : div2 x = (2⁻¹ : ℚ) • x := rfl

Interval/Approx/Dyadic.lean

@@ -28,6 +28,8 @@ instance : Repr Dyadic where
 
 instance : Div2 Dyadic where
   div2 x := x >>> 1
+
+instance : Div2Zero Dyadic where
   div2_zero := rfl
 
 lemma Dyadic.natCast_zero : (0 : ℕ) = (0 : Dyadic) := rfl