Skip to content

Commit

Permalink
fix(data/nat/basic): fix typos in docstrings (#5592)
Browse files Browse the repository at this point in the history
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
  • Loading branch information
kbuzzard and robertylewis committed Jan 4, 2021
1 parent afbf47d commit 6acf99e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/data/nat/basic.lean
Expand Up @@ -881,12 +881,12 @@ protected theorem dvd_add_right {k m n : ℕ} (h : k ∣ m) : k ∣ m + n ↔ k
@[simp] protected theorem not_two_dvd_bit1 (n : ℕ) : ¬ 2 ∣ bit1 n :=
mt (nat.dvd_add_right two_dvd_bit0).1 dec_trivial

/-- A natural number m divides the sum m + n if and only if m divides b.-/
/-- A natural number `m` divides the sum `m + n` if and only if `m` divides `n`.-/
@[simp] protected lemma dvd_add_self_left {m n : ℕ} :
m ∣ m + n ↔ m ∣ n :=
nat.dvd_add_right (dvd_refl m)

/-- A natural number m divides the sum n + m if and only if m divides b.-/
/-- A natural number `m` divides the sum `n + m` if and only if `m` divides `n`.-/
@[simp] protected lemma dvd_add_self_right {m n : ℕ} :
m ∣ n + m ↔ m ∣ n :=
nat.dvd_add_left (dvd_refl m)
Expand Down

0 comments on commit 6acf99e

Please sign in to comment.