-
Notifications
You must be signed in to change notification settings - Fork 298
/
ring.lean
599 lines (448 loc) · 23.9 KB
/
ring.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston
-/
import algebra.group
import tactic.norm_cast
/-!
# Properties and homomorphisms of semirings and rings
This file proves simple properties of semirings, rings and domains and their unit groups. It also
defines homomorphisms of semirings and rings, both unbundled (e.g. `is_semiring_hom f`)
and bundled (e.g. `ring_hom a β`, a.k.a. `α →+* β`). The unbundled ones are deprecated
and the plan is to slowly remove them from mathlib.
## Main definitions
is_semiring_hom (deprecated), is_ring_hom (deprecated), ring_hom, nonzero_comm_semiring,
nonzero_comm_ring, domain
## Notations
→+* for bundled ring homs (also use for semiring homs)
## Implementation notes
There's a coercion from bundled homs to fun, and the canonical
notation is to use the bundled hom as a function via this coercion.
There is no `semiring_hom` -- the idea is that `ring_hom` is used.
The constructor for a `ring_hom` between semirings needs a proof of `map_zero`, `map_one` and
`map_add` as well as `map_mul`; a separate constructor `ring_hom.mk'` will construct ring homs
between rings from monoid homs given only a proof that addition is preserved.
Throughout the section on `ring_hom` implicit `{}` brackets are often used instead of type class `[]` brackets.
This is done when the instances can be inferred because they are implicit arguments to the type `ring_hom`.
When they can be inferred from the type it is faster to use this method than to use type class inference.
## Tags
is_ring_hom, is_semiring_hom, ring_hom, semiring_hom, semiring, comm_semiring, ring, comm_ring,
domain, integral_domain, nonzero_comm_semiring, nonzero_comm_ring, units
-/
universes u v w
variable {α : Type u}
section
variable [semiring α]
theorem mul_two (n : α) : n * 2 = n + n :=
(left_distrib n 1 1).trans (by simp)
theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
(two_mul _).symm
@[simp] lemma mul_ite {α} [semiring α] (P : Prop) [decidable P] (a : α) :
a * (if P then 1 else 0) = if P then a else 0 :=
by split_ifs; simp
variable (α)
/-- Either zero and one are nonequal in a semiring, or the semiring is the zero ring. -/
lemma zero_ne_one_or_forall_eq_0 : (0 : α) ≠ 1 ∨ (∀a:α, a = 0) :=
by haveI := classical.dec;
refine not_or_of_imp (λ h a, _); simpa using congr_arg ((*) a) h.symm
/-- If zero equals one in a semiring, the semiring is the zero ring. -/
lemma eq_zero_of_zero_eq_one (h : (0 : α) = 1) : (∀a:α, a = 0) :=
(zero_ne_one_or_forall_eq_0 α).neg_resolve_left h
/-- If zero equals one in a semiring, all elements of that semiring are equal. -/
theorem subsingleton_of_zero_eq_one (h : (0 : α) = 1) : subsingleton α :=
⟨λa b, by rw [eq_zero_of_zero_eq_one α h a, eq_zero_of_zero_eq_one α h b]⟩
end
namespace units
variables [ring α] {a b : α}
/-- Each element of the group of units of a ring has an additive inverse. -/
instance : has_neg (units α) := ⟨λu, ⟨-↑u, -↑u⁻¹, by simp, by simp⟩ ⟩
/-- Representing an element of a ring's unit group as an element of the ring commutes with
mapping this element to its additive inverse. -/
@[simp] protected theorem coe_neg (u : units α) : (↑-u : α) = -u := rfl
/-- Mapping an element of a ring's unit group to its inverse commutes with mapping this element
to its additive inverse. -/
@[simp] protected theorem neg_inv (u : units α) : (-u)⁻¹ = -u⁻¹ := rfl
/-- An element of a ring's unit group equals the additive inverse of its additive inverse. -/
@[simp] protected theorem neg_neg (u : units α) : - -u = u :=
units.ext $ neg_neg _
/-- Multiplication of elements of a ring's unit group commutes with mapping the first
argument to its additive inverse. -/
@[simp] protected theorem neg_mul (u₁ u₂ : units α) : -u₁ * u₂ = -(u₁ * u₂) :=
units.ext $ neg_mul_eq_neg_mul_symm _ _
/-- Multiplication of elements of a ring's unit group commutes with mapping the second argument
to its additive inverse. -/
@[simp] protected theorem mul_neg (u₁ u₂ : units α) : u₁ * -u₂ = -(u₁ * u₂) :=
units.ext $ (neg_mul_eq_mul_neg _ _).symm
/-- Multiplication of the additive inverses of two elements of a ring's unit group equals
multiplication of the two original elements. -/
@[simp] protected theorem neg_mul_neg (u₁ u₂ : units α) : -u₁ * -u₂ = u₁ * u₂ := by simp
/-- The additive inverse of an element of a ring's unit group equals the additive inverse of
one times the original element. -/
protected theorem neg_eq_neg_one_mul (u : units α) : -u = -1 * u := by simp
end units
instance [semiring α] : semiring (with_zero α) :=
{ left_distrib := λ a b c, begin
cases a with a, {refl},
cases b with b; cases c with c; try {refl},
exact congr_arg some (left_distrib _ _ _)
end,
right_distrib := λ a b c, begin
cases c with c,
{ change (a + b) * 0 = a * 0 + b * 0, simp },
cases a with a; cases b with b; try {refl},
exact congr_arg some (right_distrib _ _ _)
end,
..with_zero.add_comm_monoid,
..with_zero.mul_zero_class,
..with_zero.monoid }
attribute [refl] dvd_refl
attribute [trans] dvd.trans
/-- Predicate for semiring homomorphisms (deprecated -- use the bundled `ring_hom` version). -/
class is_semiring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α → β) : Prop :=
(map_zero : f 0 = 0)
(map_one : f 1 = 1)
(map_add : ∀ {x y}, f (x + y) = f x + f y)
(map_mul : ∀ {x y}, f (x * y) = f x * f y)
namespace is_semiring_hom
variables {β : Type v} [semiring α] [semiring β]
variables (f : α → β) [is_semiring_hom f] {x y : α}
/-- The identity map is a semiring homomorphism. -/
instance id : is_semiring_hom (@id α) := by refine {..}; intros; refl
/-- The composition of two semiring homomorphisms is a semiring homomorphism. -/
instance comp {γ} [semiring γ] (g : β → γ) [is_semiring_hom g] :
is_semiring_hom (g ∘ f) :=
{ map_zero := by simp [map_zero f]; exact map_zero g,
map_one := by simp [map_one f]; exact map_one g,
map_add := λ x y, by simp [map_add f]; rw map_add g; refl,
map_mul := λ x y, by simp [map_mul f]; rw map_mul g; refl }
/-- A semiring homomorphism is an additive monoid homomorphism. -/
instance : is_add_monoid_hom f :=
{ ..‹is_semiring_hom f› }
/-- A semiring homomorphism is a monoid homomorphism. -/
instance : is_monoid_hom f :=
{ ..‹is_semiring_hom f› }
end is_semiring_hom
section
variables [ring α] (a b c d e : α)
/-- An element of a ring multiplied by the additive inverse of one is the element's additive
inverse. -/
lemma mul_neg_one (a : α) : a * -1 = -a := by simp
/-- The additive inverse of one multiplied by an element of a ring is the element's additive
inverse. -/
lemma neg_one_mul (a : α) : -1 * a = -a := by simp
/-- An iff statement following from right distributivity in rings and the definition
of subtraction. -/
theorem mul_add_eq_mul_add_iff_sub_mul_add_eq : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
calc
a * e + c = b * e + d ↔ a * e + c = d + b * e : by simp
... ↔ a * e + c - b * e = d : iff.intro (λ h, begin simp [h] end) (λ h,
begin simp [h.symm] end)
... ↔ (a - b) * e + c = d : begin simp [@sub_eq_add_neg α, @right_distrib α] end
/-- A simplification of one side of an equation exploiting right distributivity in rings
and the definition of subtraction. -/
theorem sub_mul_add_eq_of_mul_add_eq_mul_add : a * e + c = b * e + d → (a - b) * e + c = d :=
assume h,
calc
(a - b) * e + c = (a * e + c) - b * e : begin simp [@sub_eq_add_neg α, @right_distrib α] end
... = d : begin rw h, simp [@add_sub_cancel α] end
/-- If the product of two elements of a ring is nonzero, both elements are nonzero. -/
theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : α} (h : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
begin
split,
{ intro ha, apply h, simp [ha] },
{ intro hb, apply h, simp [hb] }
end
end
/-- Given an element a of a commutative semiring, there exists another element whose product
with zero equals a iff a equals zero. -/
@[simp] lemma zero_dvd_iff [comm_semiring α] {a : α} : 0 ∣ a ↔ a = 0 :=
⟨eq_zero_of_zero_dvd, λ h, by rw h⟩
section comm_ring
variable [comm_ring α]
/-- Representation of a difference of two squares in a commutative ring as a product. -/
theorem mul_self_sub_mul_self (a b : α) : a * a - b * b = (a + b) * (a - b) :=
by rw [add_mul, mul_sub, mul_sub, mul_comm a b, sub_add_sub_cancel]
/-- An element a of a commutative ring divides the additive inverse of an element b iff a
divides b. -/
@[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩
/-- The additive inverse of an element a of a commutative ring divides another element b iff a
divides b. -/
@[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
/-- If an element a divides another element c in a commutative ring, a divides the sum of another
element b with c iff a divides b. -/
theorem dvd_add_left {a b c : α} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
(dvd_add_iff_left h).symm
/-- If an element a divides another element b in a commutative ring, a divides the sum of b and
another element c iff a divides c. -/
theorem dvd_add_right {a b c : α} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c :=
(dvd_add_iff_right h).symm
/-- An element a divides the sum a + b if and only if a divides b.-/
@[simp] lemma dvd_add_self_left {a b : α} :
a ∣ a + b ↔ a ∣ b :=
dvd_add_right (dvd_refl a)
/-- An element a divides the sum b + a if and only if a divides b.-/
@[simp] lemma dvd_add_self_right {a b : α} :
a ∣ b + a ↔ a ∣ b :=
dvd_add_left (dvd_refl a)
/-- Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with
its roots. This particular version states that if we have a root `x` of a monic quadratic
polynomial, then there is another root `y` such that `x + y` is negative the `a_1` coefficient
and `x * y` is the `a_0` coefficient. -/
lemma Vieta_formula_quadratic {b c x : α} (h : x * x - b * x + c = 0) :
∃ y : α, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, mul_comm, this],
end
end comm_ring
/-- Predicate for ring homomorphisms (deprecated -- use the bundled `ring_hom` version). -/
class is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α → β) : Prop :=
(map_one : f 1 = 1)
(map_mul : ∀ {x y}, f (x * y) = f x * f y)
(map_add : ∀ {x y}, f (x + y) = f x + f y)
namespace is_ring_hom
variables {β : Type v} [ring α] [ring β]
/-- A map of rings that is a semiring homomorphism is also a ring homomorphism. -/
lemma of_semiring (f : α → β) [H : is_semiring_hom f] : is_ring_hom f := {..H}
variables (f : α → β) [is_ring_hom f] {x y : α}
/-- Ring homomorphisms map zero to zero. -/
lemma map_zero : f 0 = 0 :=
calc f 0 = f (0 + 0) - f 0 : by rw [map_add f]; simp
... = 0 : by simp
/-- Ring homomorphisms preserve additive inverses. -/
lemma map_neg : f (-x) = -f x :=
calc f (-x) = f (-x + x) - f x : by rw [map_add f]; simp
... = -f x : by simp [map_zero f]
/-- Ring homomorphisms preserve subtraction. -/
lemma map_sub : f (x - y) = f x - f y :=
by simp [map_add f, map_neg f]
/-- The identity map is a ring homomorphism. -/
instance id : is_ring_hom (@id α) := by refine {..}; intros; refl
/-- The composition of two ring homomorphisms is a ring homomorphism. -/
instance comp {γ} [ring γ] (g : β → γ) [is_ring_hom g] :
is_ring_hom (g ∘ f) :=
{ map_add := λ x y, by simp [map_add f]; rw map_add g; refl,
map_mul := λ x y, by simp [map_mul f]; rw map_mul g; refl,
map_one := by simp [map_one f]; exact map_one g }
/-- A ring homomorphism is also a semiring homomorphism. -/
instance : is_semiring_hom f :=
{ map_zero := map_zero f, ..‹is_ring_hom f› }
instance : is_add_group_hom f := { }
end is_ring_hom
set_option old_structure_cmd true
/-- Bundled semiring homomorphisms; use this for bundled ring homomorphisms too. -/
structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β]
extends monoid_hom α β, add_monoid_hom α β
infixr ` →+* `:25 := ring_hom
instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe_to_fun (α →+* β) :=
⟨_, ring_hom.to_fun⟩
instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe (α →+* β) (α →* β) :=
⟨ring_hom.to_monoid_hom⟩
instance {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : has_coe (α →+* β) (α →+ β) :=
⟨ring_hom.to_add_monoid_hom⟩
@[squash_cast] lemma coe_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a : α) :
((f : α →* β) : α → β) a = (f : α → β) a := rfl
@[squash_cast] lemma coe_add_monoid_hom {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} (f : α →+* β) (a : α) :
((f : α →+ β) : α → β) a = (f : α → β) a := rfl
namespace ring_hom
variables {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β]
include rα rβ
/-- Interpret `f : α → β` with `is_semiring_hom f` as a ring homomorphism. -/
def of (f : α → β) [is_semiring_hom f] : α →+* β :=
{ to_fun := f,
.. monoid_hom.of f,
.. add_monoid_hom.of f }
@[simp] lemma coe_of (f : α → β) [is_semiring_hom f] : ⇑(of f) = f := rfl
variables (f : α →+* β) {x y : α} {rα rβ}
theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
by cases f; cases g; cases h; refl
@[extensionality] theorem ext ⦃f g : α →+* β⦄ (h : ∀ x, f x = g x) : f = g :=
coe_inj (funext h)
theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
⟨λ h x, h ▸ rfl, λ h, ext h⟩
/-- Ring homomorphisms map zero to zero. -/
@[simp] lemma map_zero (f : α →+* β) : f 0 = 0 := f.map_zero'
/-- Ring homomorphisms map one to one. -/
@[simp] lemma map_one (f : α →+* β) : f 1 = 1 := f.map_one'
/-- Ring homomorphisms preserve addition. -/
@[simp] lemma map_add (f : α →+* β) (a b : α) : f (a + b) = f a + f b := f.map_add' a b
/-- Ring homomorphisms preserve multiplication. -/
@[simp] lemma map_mul (f : α →+* β) (a b : α) : f (a * b) = f a * f b := f.map_mul' a b
instance (f : α →+* β) : is_semiring_hom f :=
{ map_zero := f.map_zero,
map_one := f.map_one,
map_add := f.map_add,
map_mul := f.map_mul }
omit rα rβ
instance {α γ} [ring α] [ring γ] (g : α →+* γ) : is_ring_hom g :=
is_ring_hom.of_semiring g
/-- The identity ring homomorphism from a semiring to itself. -/
def id (α : Type*) [semiring α] : α →+* α :=
by refine {to_fun := id, ..}; intros; refl
include rα
@[simp] lemma id_apply : ring_hom.id α x = x := rfl
variable {rγ : semiring γ}
include rβ rγ
/-- Composition of ring homomorphisms is a ring homomorphism. -/
def comp (hnp : β →+* γ) (hmn : α →+* β) : α →+* γ :=
{ to_fun := hnp ∘ hmn,
map_zero' := by simp,
map_one' := by simp,
map_add' := λ x y, by simp,
map_mul' := λ x y, by simp}
@[simp] lemma coe_comp (hnp : β →+* γ) (hmn : α →+* β) : (hnp.comp hmn : α → γ) = hnp ∘ hmn := rfl
@[simp] lemma comp_apply (hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn : α → γ) x =
(hnp (hmn x)) := rfl
omit rα rβ rγ
/-- Ring homomorphisms preserve additive inverse. -/
@[simp] theorem map_neg {α β} [ring α] [ring β] (f : α →+* β) (x : α) : f (-x) = -(f x) :=
eq_neg_of_add_eq_zero $ by rw [←f.map_add, neg_add_self, f.map_zero]
/-- Ring homomorphisms preserve subtraction. -/
@[simp] theorem map_sub {α β} [ring α] [ring β] (f : α →+* β) (x y : α) :
f (x - y) = (f x) - (f y) := by simp
include rα
/-- Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition. -/
def mk' {γ} [ring γ] (f : α →* γ) (map_add : ∀ a b : α, f (a + b) = f a + f b) : α →+* γ :=
{ to_fun := f,
map_zero' := add_self_iff_eq_zero.1 $ by rw [←map_add, add_zero],
map_one' := f.map_one,
map_mul' := f.map_mul,
map_add' := map_add }
end ring_hom
/-- Predicate for commutative semirings in which zero does not equal one. -/
class nonzero_comm_semiring (α : Type*) extends comm_semiring α, zero_ne_one_class α
/-- Predicate for commutative rings in which zero does not equal one. -/
class nonzero_comm_ring (α : Type*) extends comm_ring α, zero_ne_one_class α
/-- A nonzero commutative ring is a nonzero commutative semiring. -/
instance nonzero_comm_ring.to_nonzero_comm_semiring {α : Type*} [I : nonzero_comm_ring α] :
nonzero_comm_semiring α :=
{ zero_ne_one := by convert zero_ne_one,
..show comm_semiring α, by apply_instance }
/-- An integral domain is a nonzero commutative ring. -/
instance integral_domain.to_nonzero_comm_ring (α : Type*) [id : integral_domain α] :
nonzero_comm_ring α :=
{ ..id }
/-- An element of the unit group of a nonzero commutative semiring represented as an element
of the semiring is nonzero. -/
lemma units.coe_ne_zero [nonzero_comm_semiring α] (u : units α) : (u : α) ≠ 0 :=
λ h : u.1 = 0, by simpa [h, zero_ne_one] using u.3
/-- Makes a nonzero commutative ring from a commutative ring containing at least two distinct
elements. -/
def nonzero_comm_ring.of_ne [comm_ring α] {x y : α} (h : x ≠ y) : nonzero_comm_ring α :=
{ one := 1,
zero := 0,
zero_ne_one := λ h01, h $ by rw [← one_mul x, ← one_mul y, ← h01, zero_mul, zero_mul],
..show comm_ring α, by apply_instance }
/-- Makes a nonzero commutative semiring from a commutative semiring containing at least two
distinct elements. -/
def nonzero_comm_semiring.of_ne [comm_semiring α] {x y : α} (h : x ≠ y) : nonzero_comm_semiring α :=
{ one := 1,
zero := 0,
zero_ne_one := λ h01, h $ by rw [← one_mul x, ← one_mul y, ← h01, zero_mul, zero_mul],
..show comm_semiring α, by apply_instance }
/-- this is needed for compatibility between Lean 3.4.2 and Lean 3.5.0c -/
def has_div_of_division_ring [division_ring α] : has_div α := division_ring_has_div
/-- A domain is a ring with no zero divisors, i.e. satisfying
the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
is an integral domain without assuming commutativity of multiplication. -/
class domain (α : Type u) extends ring α, no_zero_divisors α, zero_ne_one_class α
section domain
variable [domain α]
/-- Simplification theorems for the definition of a domain. -/
@[simp] theorem mul_eq_zero {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
⟨eq_zero_or_eq_zero_of_mul_eq_zero, λo,
or.elim o (λh, by rw h; apply zero_mul) (λh, by rw h; apply mul_zero)⟩
@[simp] theorem zero_eq_mul {a b : α} : 0 = a * b ↔ a = 0 ∨ b = 0 :=
by rw [eq_comm, mul_eq_zero]
lemma mul_self_eq_zero {α} [domain α] {x : α} : x * x = 0 ↔ x = 0 := by simp
lemma zero_eq_mul_self {α} [domain α] {x : α} : 0 = x * x ↔ x = 0 := by simp
/-- The product of two nonzero elements of a domain is nonzero. -/
theorem mul_ne_zero' {a b : α} (h₁ : a ≠ 0) (h₂ : b ≠ 0) : a * b ≠ 0 :=
λ h, or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) h₁ h₂
/-- Right multiplication by a nonzero element in a domain is injective. -/
theorem domain.mul_right_inj {a b c : α} (ha : a ≠ 0) : b * a = c * a ↔ b = c :=
by rw [← sub_eq_zero, ← mul_sub_right_distrib, mul_eq_zero];
simp [ha]; exact sub_eq_zero
/-- Left multiplication by a nonzero element in a domain is injective. -/
theorem domain.mul_left_inj {a b c : α} (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
by rw [← sub_eq_zero, ← mul_sub_left_distrib, mul_eq_zero];
simp [ha]; exact sub_eq_zero
/-- An element of a domain fixed by right multiplication by an element other than one must
be zero. -/
theorem eq_zero_of_mul_eq_self_right' {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
by apply (mul_eq_zero.1 _).resolve_right (sub_ne_zero.2 h₁);
rw [mul_sub_left_distrib, mul_one, sub_eq_zero, h₂]
/-- An element of a domain fixed by left multiplication by an element other than one must
be zero. -/
theorem eq_zero_of_mul_eq_self_left' {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 :=
by apply (mul_eq_zero.1 _).resolve_left (sub_ne_zero.2 h₁);
rw [mul_sub_right_distrib, one_mul, sub_eq_zero, h₂]
/-- For elements a, b of a domain, if a*b is nonzero, so is b*a. -/
theorem mul_ne_zero_comm' {a b : α} (h : a * b ≠ 0) : b * a ≠ 0 :=
mul_ne_zero' (ne_zero_of_mul_ne_zero_left h) (ne_zero_of_mul_ne_zero_right h)
end domain
/- integral domains -/
section
variables [s : integral_domain α] (a b c d e : α)
include s
/-- An integral domain is a domain. -/
instance integral_domain.to_domain : domain α := {..s}
/-- Right multiplcation by a nonzero element of an integral domain is injective. -/
theorem eq_of_mul_eq_mul_right_of_ne_zero {a b c : α} (ha : a ≠ 0) (h : b * a = c * a) : b = c :=
have b * a - c * a = 0, by simp [h],
have (b - c) * a = 0, by rw [mul_sub_right_distrib, this],
have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha,
eq_of_sub_eq_zero this
/-- Left multiplication by a nonzero element of an integral domain is injective. -/
theorem eq_of_mul_eq_mul_left_of_ne_zero {a b c : α} (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
have a * b - a * c = 0, by simp [h],
have a * (b - c) = 0, by rw [mul_sub_left_distrib, this],
have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha,
eq_of_sub_eq_zero this
/-- Given two elements b, c of an integral domain and a nonzero element a, a*b divides a*c iff
b divides c. -/
theorem mul_dvd_mul_iff_left {a b c : α} (ha : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c :=
exists_congr $ λ d, by rw [mul_assoc, domain.mul_left_inj ha]
/-- Given two elements a, b of an integral domain and a nonzero element c, a*c divides b*c iff
a divides b. -/
theorem mul_dvd_mul_iff_right {a b c : α} (hc : c ≠ 0) : a * c ∣ b * c ↔ a ∣ b :=
exists_congr $ λ d, by rw [mul_right_comm, domain.mul_right_inj hc]
/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
one's additive inverse. -/
lemma units.inv_eq_self_iff (u : units α) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
by conv {to_lhs, rw [inv_eq_iff_mul_eq_one, ← mul_one (1 : units α), units.ext_iff, units.coe_mul,
units.coe_mul, mul_self_eq_mul_self_iff, ← units.ext_iff, ← units.coe_neg, ← units.ext_iff] }
end
/- units in various rings -/
namespace units
section comm_semiring
variables [comm_semiring α] (a b : α) (u : units α)
/-- Elements of the unit group of a commutative semiring represented as elements of the semiring
divide any element of the semiring. -/
@[simp] lemma coe_dvd : ↑u ∣ a := ⟨↑u⁻¹ * a, by simp⟩
/-- In a commutative semiring, an element a divides an element b iff a divides all
associates of b. -/
@[simp] lemma dvd_coe_mul : a ∣ b * u ↔ a ∣ b :=
iff.intro
(assume ⟨c, eq⟩, ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, units.mul_inv_cancel_right]⟩)
(assume ⟨c, eq⟩, eq.symm ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
/-- An element of a commutative semiring divides a unit iff the element divides one. -/
@[simp] lemma dvd_coe : a ∣ ↑u ↔ a ∣ 1 :=
suffices a ∣ 1 * ↑u ↔ a ∣ 1, by simpa,
dvd_coe_mul _ _ _
/-- In a commutative semiring, an element a divides an element b iff all associates of a divide b.-/
@[simp] lemma coe_mul_dvd : a * u ∣ b ↔ a ∣ b :=
iff.intro
(assume ⟨c, eq⟩, ⟨c * ↑u, eq.symm ▸ by ac_refl⟩)
(assume h, suffices a * ↑u ∣ b * 1, by simpa, mul_dvd_mul h (coe_dvd _ _))
end comm_semiring
section domain
variables [domain α]
/-- Every unit in a domain is nonzero. -/
@[simp] theorem ne_zero : ∀(u : units α), (↑u : α) ≠ 0
| ⟨u, v, (huv : 0 * v = 1), hvu⟩ rfl := by simpa using huv
end domain
end units