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

feat(library/algebra/ring): simplify ring theorems using rewrite tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 18:48:02 -08:00
parent 0ae6e2b3e4
commit 96c161a659
1 changed files with 4 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/algebra/ring.lean
View file

@ -133,12 +133,8 @@ section comm_semiring
dvd.elim dvd_cd
(take f, assume Hcfd : d = c * f,
dvd.intro
(calc
a * c * (e * f) = a * (c * (e * f)) : mul.assoc
... = a * (e * (c * f)) : mul.left_comm
... = a * e * (c * f) : (!mul.assoc)⁻¹
... = b * (c * f) : Haeb
... = b * d : Hcfd)))
(show a * c * (e * f) = b * d,
by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc, Haeb, Hcfd])))
theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b | c) : a | c :=
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
@ -151,7 +147,8 @@ section comm_semiring
(take d, assume Hadb : b = a * d,
dvd.elim Hac
(take e, assume Haec : c = a * e,
dvd.intro (show a * (d + e) = b + c, from Hadb⁻¹ ▸ Haec⁻¹ ▸ left_distrib a d e)))
dvd.intro (show a * (d + e) = b + c,
by rewrite [left_distrib, -Hadb, -Haec])))
end comm_semiring
/- ring -/