michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/ring): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-03 20:07:12 -08:00
parent cb12b9b876
commit 790dbc53c3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/algebra/ring.lean
View file

@ -51,12 +51,12 @@ section semiring
theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
suppose a = 0,
have a * b = 0, from this⁻¹ ▸ zero_mul b,
have a * b = 0, by rewrite [this, zero_mul],
H this
theorem ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
suppose b = 0,
have a * b = 0, from this⁻¹ ▸ mul_zero a,
have a * b = 0, by rewrite [this, mul_zero],
H this
local attribute right_distrib [simp]
@ -86,7 +86,7 @@ section comm_semiring
theorem dvd_of_mul_right_eq {a b c : A} (H : a * c = b) : a ∣ b := dvd.intro H
theorem dvd.intro_left {a b c : A} (H : c * a = b) : a ∣ b :=
dvd.intro (!mul.comm ▸ H)
dvd.intro (by rewrite mul.comm at H; exact H)
theorem dvd_of_mul_left_eq {a b c : A} (H : c * a = b) : a ∣ b := dvd.intro_left H