From 8bb8c20fab05747b4f8ab53d36de72823ba3870b Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 30 Dec 2024 08:54:46 +0900
Subject: [PATCH] =?UTF-8?q?`ring`=20=E3=81=AB=E3=81=A4=E3=81=84=E3=81=A6?=
 =?UTF-8?q?=E3=81=AE=E3=82=B3=E3=83=A1=E3=83=B3=E3=83=88=E3=81=8C=E9=96=93?=
 =?UTF-8?q?=E9=81=95=E3=81=A3=E3=81=A6=E3=81=84=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

自然数が環ではなくても、半環なので ring は使うことができる
---
 LeanByExample/Tactic/RwSearch.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanByExample/Tactic/RwSearch.lean b/LeanByExample/Tactic/RwSearch.lean
index af85eba6..065f1a0c 100644
--- a/LeanByExample/Tactic/RwSearch.lean
+++ b/LeanByExample/Tactic/RwSearch.lean
@@ -10,7 +10,7 @@ variable (m n : ℕ)
 set_option says.verify true
 
 example : (m - n) - n = m - 2 * n := by
-  -- `ring` では示せない。自然数は環ではないので当然
+  -- `ring` では示せない。自然数の引き算は環の公理を満たさないから
   fail_if_success solve
   | ring