文章校正

LeanByExample/Declarative/Inductive.lean

@@ -179,7 +179,7 @@ Peano の公理とは、次のようなものです:
 * `succ` 関数は単射。つまり2つの異なる自然数 `n` と `m` に対して `succ n ≠ succ m` が成り立つ。
 * 帰納法の原理が成り立つ。つまり、任意の述語 `P : ℕ → Prop` に対して `P 0` かつ `∀ n : ℕ, P n → P (succ n)` ならば `∀ n : ℕ, P n` が成り立つ。
 
-これを `inductive` を使用して再現すると次のようになります。
+これを `inductive` コマンドを使用して再現すると次のようになります。
 -/
 
 /-- Peano の公理によって定義された自然数 -/