From eca3437388c9b15344719c4625566685253eb2e2 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 9 Aug 2015 21:23:44 -0400 Subject: [PATCH] refactor(library/algebra/ring): add alternate names for dvd.intro, dvd.intro_left --- library/algebra/ring.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index aa2d29e56..7a4f5ff82 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -78,9 +78,13 @@ section comm_semiring theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b := exists.intro _ H⁻¹ + 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) + theorem dvd_of_mul_left_eq {a b c : A} (H : c * a = b) : a ∣ b := dvd.intro_left H + theorem exists_eq_mul_right_of_dvd {a b : A} (H : a ∣ b) : ∃c, b = a * c := H theorem dvd.elim {P : Prop} {a b : A} (H₁ : a ∣ b) (H₂ : ∀c, b = a * c → P) : P :=