Update S01_Basics.lean

Corrected translation of '模块' to '模'.

Author: hewzhew

MIL/C07_Hierarchies/S01_Basics.lean

@@ -505,7 +505,7 @@ all remaining arguments have metavariables: Ring₃ ?R @Module₁ ?R ?inst✝ M`
  ``Module₁.toSMul₃ : {R : Type} →  [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M``
 其最终结果 ``SMul₃ R M`` 同时提到了 ``R`` 和 ``M`` ，所以这个字段可以安全地用作实例。规则很容易记住：在 ``extends`` 子句中出现的每个类都应提及参数中出现的每个类型。
 
-让我们创建我们的第一个模块实例：一个环自身就是一个模块，其乘法作为标量乘法。
+让我们创建我们的第一个模实例：一个环自身就是一个模，其乘法作为标量乘法。
 BOTH: -/
 -- QUOTE:
 instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
@@ -517,7 +517,7 @@ instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
   smul_add := Ring₃.left_distrib
 -- QUOTE.
 /- TEXT:
-作为第二个例子，每个阿贝尔群都是整数环上的模块（这是推广向量空间理论以允许非可逆标量的原因之一）。首先，对于任何配备零和加法的类型，都可以定义自然数的标量乘法： ``n • a`` 定义为 ``a + ⋯ + a`` ，其中 ``a`` 出现 ``n`` 次。然后通过确保 ``(-1) • a = -a`` 将其扩展到整数的标量乘法。
+作为第二个例子，每个阿贝尔群都是整数环上的模（这是推广向量空间理论以允许非可逆标量的原因之一）。首先，对于任何配备零和加法的类型，都可以定义自然数的标量乘法： ``n • a`` 定义为 ``a + ⋯ + a`` ，其中 ``a`` 出现 ``n`` 次。然后通过确保 ``(-1) • a = -a`` 将其扩展到整数的标量乘法。
 BOTH: -/
 -- QUOTE:
 
@@ -530,7 +530,7 @@ def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
   | Int.negSucc n, a => -nsmul₁ n.succ a
 -- QUOTE.
 /- TEXT:
-证明这会产生一个模块结构有点繁琐，且对当前讨论来说不那么有趣，所以我们很抱歉地略过所有公理。您**无需**用证明来替换这些抱歉。如果您坚持这样做，那么您可能需要陈述并证明关于 ``nsmul₁`` 和 ``zsmul₁`` 的几个中间引理。
+证明这会产生一个模结构有点繁琐，且对当前讨论来说不那么有趣，所以我们很抱歉地略过所有公理。您**无需**用证明来替换这些抱歉。如果您坚持这样做，那么您可能需要陈述并证明关于 ``nsmul₁`` 和 ``zsmul₁`` 的几个中间引理。
 BOTH: -/
 -- QUOTE:
 
@@ -543,7 +543,7 @@ instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
   smul_add := sorry
 -- QUOTE.
 /- TEXT:
-一个更为重要的问题是，我们目前对于整数环 ``ℤ`` 本身存在两种模块结构：首先，由于 ``ℤ`` 是阿贝尔群，因此可以定义其为 ``abGrpModule ℤ`` ；其次，鉴于 ``ℤ`` 作为环的性质，我们也可以将其视作 ``selfModule ℤ`` 。这两种模块结构虽然对应相同的阿贝尔群结构，但它们在标量乘法上的一致性并不显而易见。实际上，这两者确实是相同的，但这一点并非由定义直接决定，而需要通过证明来确认。这一情况对类型类实例解析过程而言无疑是个不利消息，并且可能会让使用此层次结构的用户感到颇为沮丧。当我们直接请求找到某个实例时，Lean 会自动选择一个，我们可以通过以下命令查看所选的是哪一个：
+一个更为重要的问题是，我们目前对于整数环 ``ℤ`` 本身存在两种模结构：首先，由于 ``ℤ`` 是阿贝尔群，因此可以定义其为 ``abGrpModule ℤ`` ；其次，鉴于 ``ℤ`` 作为环的性质，我们也可以将其视作 ``selfModule ℤ`` 。这两种模结构虽然对应相同的阿贝尔群结构，但它们在标量乘法上的一致性并不显而易见。实际上，这两者确实是相同的，但这一点并非由定义直接决定，而需要通过证明来确认。这一情况对类型类实例解析过程而言无疑是个不利消息，并且可能会让使用此层次结构的用户感到颇为沮丧。当我们直接请求找到某个实例时，Lean 会自动选择一个，我们可以通过以下命令查看所选的是哪一个：
 BOTH: -/
 -- QUOTE:
 
@@ -555,7 +555,7 @@ BOTH: -/
 
 重要的是要明白，并非所有的菱形结构都是不好的。实际上，在 Mathlib 中以及本章中到处都有菱形结构。在最开始的时候我们就看到，可以从 ``Monoid₁ α`` 通过 ``Semigroup₁ α`` 或者 ``DiaOneClass₁ α`` 到达 ``Dia₁ α`` ，并且由于 ``class`` 命令所做的工作，这两个 ``Dia₁ α`` 实例在定义上是相等的。特别是，底部为 ``Prop`` 值类的菱形结构不可能是不好的，因为对同一陈述的任何两个证明在定义上都是相等的。
 
-但是我们用模块创建的菱形肯定是有问题的。问题出在 ``smul`` 字段上，它是数据而非证明，并且我们有两个构造在定义上并不相等。解决这个问题的稳健方法是确保从丰富结构到贫乏结构的转换总是通过遗忘数据来实现，而不是通过定义数据。这种众所周知的模式被称为“遗忘继承”，在 https://inria.hal.science/hal-02463336 中有大量讨论。
+但是我们用模创建的菱形肯定是有问题的。问题出在 ``smul`` 字段上，它是数据而非证明，并且我们有两个构造在定义上并不相等。解决这个问题的稳健方法是确保从丰富结构到贫乏结构的转换总是通过遗忘数据来实现，而不是通过定义数据。这种众所周知的模式被称为“遗忘继承”，在 https://inria.hal.science/hal-02463336 中有大量讨论。
 
 在我们的具体案例中，我们可以修改 ``AddMonoid₃`` 的定义，以包含一个 ``nsmul`` 数据字段以及一些值为 ``Prop`` 类型的字段，以确保此操作确实是我们在上面构造的那个。在下面的定义中，这些字段在其类型后面使用 ``:=`` 给出了默认值。由于这些默认值的存在，大多数实例的构造方式与我们之前的定义完全相同。但在 ``ℤ`` 的特殊情况下，我们将能够提供特定的值。
 BOTH: -/