feat: add ContinuousMul instance on Icc 0 1 (#37786)

Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>

Author: NoahW314

Mathlib/Algebra/Order/Interval/Set/Instances.lean

@@ -6,7 +6,9 @@ Authors: Stuart Presnell, Eric Wieser, Yaël Dillies, Patrick Massot, Kim Morris
 module
 
 public import Mathlib.Algebra.GroupWithZero.InjSurj
+public import Mathlib.Algebra.GroupWithZero.Hom
 public import Mathlib.Algebra.Order.Ring.Defs
+public import Mathlib.Algebra.Group.Hom.Defs
 public import Mathlib.Algebra.Ring.Regular
 public import Mathlib.Order.Interval.Set.Basic
 public import Mathlib.Tactic.FastInstance
@@ -143,6 +145,14 @@ instance instIsCancelMulZero {R : Type*} [Ring R] [PartialOrder R] [IsOrderedRin
   @Function.Injective.isCancelMulZero _ R _ _ _ _ _ Subtype.coe_injective coe_zero coe_mul
     NoZeroDivisors.toIsCancelMulZero
 
+/-- The coercion from `Set.Icc 0 1` as a `MonoidWithZeroHom`. -/
+@[simps]
+def coeMonoidWithZeroHom : (Icc (0 : R) 1) →*₀ R where
+  toFun := (↑)
+  map_mul' := coe_mul
+  map_one' := rfl
+  map_zero' := rfl
+
 variable {β : Type*} [Ring β] [PartialOrder β] [IsOrderedRing β]
 
 theorem one_sub_mem {t : β} (ht : t ∈ Icc (0 : β) 1) : 1 - t ∈ Icc (0 : β) 1 := by
@@ -208,6 +218,12 @@ instance instCommSemigroup {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrde
     CommSemigroup (Ico (0 : R) 1) := fast_instance%
   Subtype.coe_injective.commSemigroup _ coe_mul
 
+/-- The coercion from `Set.Ico 0 1` as a `MulHom`. -/
+@[simps]
+def coeMulHom : (Ico (0 : R) 1) →ₙ* R where
+  toFun := (↑)
+  map_mul' := coe_mul
+
 end Set.Ico
 
 end OrderedSemiring
@@ -290,6 +306,13 @@ instance instCancelCommMonoid {R : Type*} [CommRing R] [PartialOrder R] [IsStric
     CancelCommMonoid (Ioc (0 : R) 1) :=
   { Set.Ioc.instCommMonoid, Set.Ioc.instCancelMonoid with }
 
+/-- The coercion from `Set.Ioc 0 1` as a `MonoidHom`. -/
+@[simps]
+def coeMonoidHom : (Ioc (0 : R) 1) →* R where
+  toFun := (↑)
+  map_mul' := coe_mul
+  map_one' := rfl
+
 end Set.Ioc
 
 /-! ### Instances for `↥(Set.Ioo 0 1)` -/
@@ -320,6 +343,12 @@ instance instCommSemigroup {R : Type*} [CommSemiring R] [PartialOrder R] [IsStri
     CommSemigroup (Ioo (0 : R) 1) := fast_instance%
   Subtype.coe_injective.commSemigroup _ coe_mul
 
+/-- The coercion from `Set.Ioo 0 1` as a `MulHom`. -/
+@[simps]
+def coeMulHom : (Ioo (0 : R) 1) →ₙ* R where
+  toFun := (↑)
+  map_mul' := coe_mul
+
 variable {β : Type*} [Ring β] [PartialOrder β] [IsOrderedRing β]
 
 theorem one_sub_mem {t : β} (ht : t ∈ Ioo (0 : β) 1) : 1 - t ∈ Ioo (0 : β) 1 := by

Mathlib/Topology/Algebra/Algebra.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Subalgebra.Lattice
 public import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Algebra.Order.Interval.Set.Instances
 
 /-!
 # Topological (sub)algebras
@@ -63,6 +64,22 @@ instance Subalgebra.continuousSMul (S : Subalgebra R A) (X) [TopologicalSpace X]
     [ContinuousSMul A X] : ContinuousSMul S X :=
   Subsemiring.continuousSMul S.toSubsemiring X
 
+instance [PartialOrder A] [IsOrderedRing A] [ContinuousMul A] :
+    ContinuousMul (Icc (0 : A) 1) :=
+  Topology.IsInducing.subtypeVal.continuousMul Icc.coeMonoidWithZeroHom
+
+instance [PartialOrder A] [IsOrderedRing A] [ContinuousMul A] :
+    ContinuousMul (Ico (0 : A) 1) :=
+  Topology.IsInducing.subtypeVal.continuousMul Ico.coeMulHom
+
+instance [PartialOrder A] [IsStrictOrderedRing A] [ContinuousMul A] :
+    ContinuousMul (Ioc (0 : A) 1) :=
+  Topology.IsInducing.subtypeVal.continuousMul Ioc.coeMonoidHom
+
+instance [PartialOrder A] [IsStrictOrderedRing A] [ContinuousMul A] :
+    ContinuousMul (Ioo (0 : A) 1) :=
+  Topology.IsInducing.subtypeVal.continuousMul Ioo.coeMulHom
+
 section
 variable [ContinuousSMul R A]