refactor(Algebra/Module): Move Module.ofCore to a MinimalAxioms fil…

…e, and rename it `ofMinimalAxioms` (#8853)

This makes it consistent with Ring, Field and Group.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib.lean

@@ -314,6 +314,7 @@ import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
 import Mathlib.Algebra.Module.LinearMap
 import Mathlib.Algebra.Module.LocalizedModule
+import Mathlib.Algebra.Module.MinimalAxioms
 import Mathlib.Algebra.Module.Opposites
 import Mathlib.Algebra.Module.PID
 import Mathlib.Algebra.Module.Pi

Mathlib/Algebra/Module/Basic.lean

@@ -225,34 +225,8 @@ theorem AddMonoid.End.int_cast_def (z : ℤ) :
   rfl
 #align add_monoid.End.int_cast_def AddMonoid.End.int_cast_def
 
-/-- A structure containing most informations as in a module, except the fields `zero_smul`
-and `smul_zero`. As these fields can be deduced from the other ones when `M` is an `AddCommGroup`,
-this provides a way to construct a module structure by checking less properties, in
-`Module.ofCore`. -/
--- Porting note: removed @[nolint has_nonempty_instance]
-structure Module.Core extends SMul R M where
-  /-- Scalar multiplication distributes over addition from the left. -/
-  smul_add : ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y
-  /-- Scalar multiplication distributes over addition from the right. -/
-  add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
-  /-- Scalar multiplication distributes over multiplication from the right. -/
-  mul_smul : ∀ (r s : R) (x : M), (r * s) • x = r • s • x
-  /-- Scalar multiplication by one is the identity. -/
-  one_smul : ∀ x : M, (1 : R) • x = x
-#align module.core Module.Core
-
 variable {R M}
 
-/-- Define `Module` without proving `zero_smul` and `smul_zero` by using an auxiliary
-structure `Module.Core`, when the underlying space is an `AddCommGroup`. -/
-def Module.ofCore (H : Module.Core R M) : Module R M :=
-  letI := H.toSMul
-  { H with
-    zero_smul := fun x =>
-      (AddMonoidHom.mk' (fun r : R => r • x) fun r s => H.add_smul r s x).map_zero
-    smul_zero := fun r => (AddMonoidHom.mk' ((· • ·) r) (H.smul_add r)).map_zero }
-#align module.of_core Module.ofCore
-
 theorem Convex.combo_eq_smul_sub_add [Module R M] {x y : M} {a b : R} (h : a + b = 1) :
     a • x + b • y = b • (y - x) + x :=
   calc

Mathlib/Algebra/Module/MinimalAxioms.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Martin C. Martin
+-/
+import Mathlib.Algebra.Module.Basic
+
+/-!
+# Minimal Axioms for a Module
+
+This file defines a constructor to define a `Module` structure on a Type with an
+`AddCommGroup`, while proving a minimum number of equalities.
+
+## Main Definitions
+
+* `Module.ofMinimalAxioms`: Define a `Module` structure on a Type with an
+  AddCommGroup by proving a minimized set of axioms
+
+-/
+
+universe u v
+
+/-- Define a `Module` structure on a Type by proving a minimized set of axioms. -/
+@[reducible]
+def Module.ofMinimalAxioms {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [SMul R M]
+    -- Scalar multiplication distributes over addition from the left.
+    (smul_add : ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y)
+    -- Scalar multiplication distributes over addition from the right.
+    (add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x)
+    -- Scalar multiplication distributes over multiplication from the right.
+    (mul_smul : ∀ (r s : R) (x : M), (r * s) • x = r • s • x)
+    -- Scalar multiplication by one is the identity.
+    (one_smul : ∀ x : M, (1 : R) • x = x) : Module R M :=
+  { smul_add := smul_add,
+    add_smul := add_smul,
+    mul_smul := mul_smul,
+    one_smul := one_smul,
+    zero_smul := fun x =>
+      (AddMonoidHom.mk' (fun r : R => r • x) fun r s => add_smul r s x).map_zero
+    smul_zero := fun r => (AddMonoidHom.mk' ((· • ·) r) (smul_add r)).map_zero }
+#align module.of_core Module.ofMinimalAxioms

Mathlib/Topology/ContinuousFunction/Bounded.lean

@@ -9,6 +9,7 @@ import Mathlib.Analysis.NormedSpace.Star.Basic
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Topology.ContinuousFunction.Algebra
 import Mathlib.Topology.MetricSpace.Equicontinuity
+import Mathlib.Algebra.Module.MinimalAxioms
 
 #align_import topology.continuous_function.bounded from "leanprover-community/mathlib"@"5dc275ec639221ca4d5f56938eb966f6ad9bc89f"
 
@@ -1411,11 +1412,11 @@ instance hasSmul' : SMul (α →ᵇ 𝕜) (α →ᵇ β) where
 #align bounded_continuous_function.has_smul' BoundedContinuousFunction.hasSmul'
 
 instance module' : Module (α →ᵇ 𝕜) (α →ᵇ β) :=
-  Module.ofCore <|
-    { smul_add := fun _ _ _ => ext fun _ => smul_add _ _ _
-      add_smul := fun _ _ _ => ext fun _ => add_smul _ _ _
-      mul_smul := fun _ _ _ => ext fun _ => mul_smul _ _ _
-      one_smul := fun f => ext fun x => one_smul 𝕜 (f x) }
+  Module.ofMinimalAxioms
+      (fun _ _ _ => ext fun _ => smul_add _ _ _)
+      (fun _ _ _ => ext fun _ => add_smul _ _ _)
+      (fun _ _ _ => ext fun _ => mul_smul _ _ _)
+      (fun f => ext fun x => one_smul 𝕜 (f x))
 #align bounded_continuous_function.module' BoundedContinuousFunction.module'
 
 /- TODO: When `NormedModule` has been added to `Analysis.NormedSpace.Basic`, this