diff --git a/GLOSSARY.md b/GLOSSARY.md
index 3b9c14c8..df176d3e 100644
--- a/GLOSSARY.md
+++ b/GLOSSARY.md
@@ -39,6 +39,7 @@
 | cycle | 巡回置換 |
 | dense | 稠密 |
 | dependent type theory | 依存型理論 |
+| definitional equality | 定義上の等しさ |
 | derivative function | 導関数 |
 | derivative of ~ | ~での微分係数 |
 | descend | （自然な全単射などへ）誘導される |
@@ -166,7 +167,7 @@
 | univariate polynomial | 一変数多項式 |
 | universal property | 普遍性 |
 | universal quantifier | 全称量化子 |
-| up to definitional equality | 定義上の同値を除いて（ベーシック圏論にてunique up to isomorphismを「同型を除いて一意」と訳されていることに合わせた） |
+| up to definitional equality | 定義上の等しさを除いて（ベーシック圏論にてunique up to isomorphismを「同型を除いて一意」と訳されていることに合わせた） |
 | well-founded | 整礎関係 |
 | well-formed | 合法 |
 | well-formed formula | 論理式 |
diff --git a/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean b/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
index 29e14e0c..9118c62e 100644
--- a/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
+++ b/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
@@ -498,7 +498,7 @@ OMIT. -/
 /- TEXT:
 .. index:: rfl, reflexivity, tactics ; refl and reflexivity, definitional equality
 
-証明項 ``rfl`` は「反射性（reflexivity）」の略です．これを ``a - b = a + -b`` の証明として提示すると，Leanはその定義を展開し，両辺が同じであることを認識します．``rfl`` タクティクもこれと同様です．これは *definitional equality(定義からの等価性)* として知られているLeanの基礎にある論理の一例です．つまり ``sub_eq_add_neg`` を用いて等式 ``a - b = a + -b`` を示せるだけでなく，実数を扱うときなど文脈によってはこの等式の両辺を同じ意味で使うことができます．ここまでの情報で，例えば前節の定理 ``self_sub`` はもう証明できます:
+証明項 ``rfl`` は「反射性（reflexivity）」の略です．これを ``a - b = a + -b`` の証明として提示すると，Leanはその定義を展開し，両辺が同じであることを認識します．``rfl`` タクティクもこれと同様です．これは *definitional equality(定義上の等しさ)* として知られているLeanの基礎にある論理の一例です．つまり ``sub_eq_add_neg`` を用いて等式 ``a - b = a + -b`` を示せるだけでなく，実数を扱うときなど文脈によってはこの等式の両辺を同じ意味で使うことができます．ここまでの情報で，例えば前節の定理 ``self_sub`` はもう証明できます:
 
 TEXT. -/
 -- BOTH:
diff --git a/MIL/C08_Groups_and_Rings/S01_Groups.lean b/MIL/C08_Groups_and_Rings/S01_Groups.lean
index 0f43ee14..81a032bd 100644
--- a/MIL/C08_Groups_and_Rings/S01_Groups.lean
+++ b/MIL/C08_Groups_and_Rings/S01_Groups.lean
@@ -1079,7 +1079,7 @@ is not enough to make the corresponding quotients equal. However the universal p
 an isomorphism in this case.
 OMIT. -/
 /- TEXT:
-1つ気に留めるべき微妙な点は型 ``G ⧸ N`` は ``N`` に（定義上の同値を除いて）本当に依存しているということであり，そのため2つの正規部分群 ``N`` と ``M`` が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型を与えます．
+1つ気に留めるべき微妙な点は型 ``G ⧸ N`` は ``N`` に（定義上の等しさを除いて）本当に依存しているということであり，そのため2つの正規部分群 ``N`` と ``M`` が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型を与えます．
 EXAMPLES: -/
 -- QUOTE:
 example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
diff --git a/MIL/C08_Groups_and_Rings/S02_Rings.lean b/MIL/C08_Groups_and_Rings/S02_Rings.lean
index 220713c8..8e50d188 100644
--- a/MIL/C08_Groups_and_Rings/S02_Rings.lean
+++ b/MIL/C08_Groups_and_Rings/S02_Rings.lean
@@ -246,7 +246,7 @@ enough to make the corresponding quotients equal. However, the universal propert
 an isomorphism in this case.
 OMIT. -/
 /- TEXT:
-微妙な点として，型 ``R ⧸ I`` は実際に ``I`` に（定義上の同値を除いて）依存するため，2つのイデアル ``I`` と ``J`` が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型性を提供します．
+微妙な点として，型 ``R ⧸ I`` は実際に ``I`` に（定義上の等しさを除いて）依存するため，2つのイデアル ``I`` と ``J`` が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型性を提供します．
 EXAMPLES: -/
 -- QUOTE:
 example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=