From ad349f59d1c6255b47f550f6047a83c7e2f49298 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Fri, 10 Jan 2025 13:16:15 +0000
Subject: [PATCH] feat: multiplication of intervals in rings

---
 Mathlib/Algebra/Order/Interval/Basic.lean | 37 ++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Order/Interval/Basic.lean b/Mathlib/Algebra/Order/Interval/Basic.lean
index a8d682494ed1f..cce6ecf518cb9 100644
--- a/Mathlib/Algebra/Order/Interval/Basic.lean
+++ b/Mathlib/Algebra/Order/Interval/Basic.lean
@@ -121,7 +121,7 @@ section Mul
 variable [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α]
 
 @[to_additive]
-instance : Mul (NonemptyInterval α) :=
+instance NonemptyInterval.instMul : Mul (NonemptyInterval α) :=
   ⟨fun s t => ⟨s.toProd * t.toProd, mul_le_mul' s.fst_le_snd t.fst_le_snd⟩⟩
 
 @[to_additive]
@@ -529,6 +529,41 @@ instance divisionCommMonoid : DivisionCommMonoid (Interval α) :=
 
 end Interval
 
+namespace NonemptyInterval
+variable [LinearOrderedSemiring α]
+
+/-- Unlike `NonemptyInterval.instMul`, this works for semirings. -/
+instance instMulOfSemiring : Mul (NonemptyInterval α) where
+  mul a b :=
+    { fst := a.fst * b.fst ⊓ a.fst * b.snd ⊓ a.snd * b.fst ⊓ a.snd * b.snd
+      snd := a.fst * b.fst ⊔ a.fst * b.snd ⊔ a.snd * b.fst ⊔ a.snd * b.snd
+      fst_le_snd := by
+        dsimp
+        apply inf_le_sup.trans ?_
+        gcongr
+        apply inf_le_sup.trans ?_
+        gcongr
+        apply inf_le_sup.trans ?_
+        rfl }
+
+/-- `fst_mul` for rings. -/
+@[simp] theorem fst_mul' (a b : NonemptyInterval α) :
+  (a * b).fst = a.fst * b.fst ⊓ a.fst * b.snd ⊓ a.snd * b.fst ⊓ a.snd * b.snd := rfl
+
+/-- `fst_mul` for rings. -/
+@[simp] theorem snd_mul' (a b : NonemptyInterval α) :
+  (a * b).snd = a.fst * b.fst ⊔ a.fst * b.snd ⊔ a.snd * b.fst ⊔ a.snd * b.snd := rfl
+
+instance : MulZeroOneClass (NonemptyInterval α) where
+  mul_zero a := by ext <;> simp
+  zero_mul a := by ext <;> simp
+  mul_one a := by ext <;> simp [a.fst_le_snd]
+  one_mul a := by ext <;> simp [a.fst_le_snd]
+
+-- TODO: Semiring (NonemptyInterval α)
+
+end NonemptyInterval
+
 section Length
 
 variable [OrderedAddCommGroup α]