-
Notifications
You must be signed in to change notification settings - Fork 307
/
Instances.lean
46 lines (42 loc) · 2.04 KB
/
Instances.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
/-
Copyright (c) 2018 Louis Carlin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Louis Carlin, Mario Carneiro
-/
import Mathlib.Algebra.EuclideanDomain.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.GroupWithZero.Units.Basic
import Mathlib.Data.Int.Order.Basic
#align_import algebra.euclidean_domain.instances from "leanprover-community/mathlib"@"e1bccd6e40ae78370f01659715d3c948716e3b7e"
/-!
# Instances for Euclidean domains
* `Int.euclideanDomain`: shows that `ℤ` is a Euclidean domain.
* `Field.toEuclideanDomain`: shows that any field is a Euclidean domain.
-/
instance Int.euclideanDomain : EuclideanDomain ℤ :=
{ inferInstanceAs (CommRing Int), inferInstanceAs (Nontrivial Int) with
quotient := (· / ·), quotient_zero := Int.ediv_zero, remainder := (· % ·),
quotient_mul_add_remainder_eq := Int.ediv_add_emod,
r := fun a b => a.natAbs < b.natAbs,
r_wellFounded := (measure natAbs).wf
remainder_lt := fun a b b0 => Int.ofNat_lt.1 <| by
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
exact Int.emod_lt _ b0
mul_left_not_lt := fun a b b0 =>
not_lt_of_ge <| by
rw [← mul_one a.natAbs, Int.natAbs_mul]
rw [← Int.natAbs_pos] at b0
exact Nat.mul_le_mul_left _ b0 }
-- see Note [lower instance priority]
instance (priority := 100) Field.toEuclideanDomain {K : Type*} [Field K] : EuclideanDomain K :=
{ toCommRing := Field.toCommRing
quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
quotient_mul_add_remainder_eq := fun a b => by
by_cases h : b = 0 <;> simp [h, mul_div_cancel₀]
r := fun a b => a = 0 ∧ b ≠ 0,
r_wellFounded :=
WellFounded.intro fun a =>
(Acc.intro _) fun b ⟨hb, _⟩ => (Acc.intro _) fun c ⟨_, hnb⟩ => False.elim <| hnb hb,
remainder_lt := fun a b hnb => by simp [hnb],
mul_left_not_lt := fun a b hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }
#align field.to_euclidean_domain Field.toEuclideanDomain