doc: fix mispelling of subtraction (#1659)

This forward-ports leanprover-community/mathlib#18145
leanprover-community · Jan 19, 2023 · 7d706cd · 7d706cd
1 parent dd4871d
commit 7d706cd
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Data/Nat/Dist.lean b/Mathlib/Data/Nat/Dist.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.nat.dist
-! leanprover-community/mathlib commit ee0c179cd3c8a45aa5bffbf1b41d8dbede452865
+! leanprover-community/mathlib commit 318fa77a2ba140a221a5b6cabae466ba855c2ffc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,7 +13,7 @@ import Mathlib.Data.Nat.Order.Basic
 /-!
 #  Distance function on ℕ
 
-This file defines a simple distance function on naturals from truncated substraction.
+This file defines a simple distance function on naturals from truncated subtraction.
 -/
 
 

diff --git a/Mathlib/Tactic/Zify/Attr.lean b/Mathlib/Tactic/Zify/Attr.lean
@@ -8,5 +8,5 @@ import Lean.Meta.Tactic.Simp.SimpTheorems
 /-! # Internal simp attribute for `zify` tactic -/
 
 /-- The simpset `zify_simps` is used by the tactic `zify` to moved expression from `ℕ` to `ℤ`
-which gives a well-behaved substraction. -/
+which gives a well-behaved subtraction. -/
 register_simp_attr zify_simps