343 lines
14 KiB
Text
343 lines
14 KiB
Text
/-
|
||
Copyright (c) 2014 Robert Lewis. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
||
Module: algebra.field
|
||
Authors: Robert Lewis
|
||
|
||
Structures with multiplicative and additive components, including division rings and fields.
|
||
The development is modeled after Isabelle's library.
|
||
-/
|
||
----------------------------------------------------------------------------------------------------
|
||
import logic.eq logic.connectives data.unit data.sigma data.prod
|
||
import algebra.function algebra.binary algebra.group algebra.ring
|
||
open eq eq.ops
|
||
|
||
namespace algebra
|
||
|
||
variable {A : Type}
|
||
|
||
structure division_ring [class] (A : Type) extends ring A, has_inv A :=
|
||
(mul_inv_cancel : ∀{a}, a ≠ zero → mul a (inv a) = one)
|
||
(inv_mul_cancel : ∀{a}, a ≠ zero → mul (inv a) a = one)
|
||
|
||
section division_ring
|
||
variables [s : division_ring A] {a b c : A}
|
||
include s
|
||
|
||
definition divide (a b : A) : A := a * b⁻¹
|
||
infix `/` := divide
|
||
|
||
-- only in this file
|
||
local attribute divide [reducible]
|
||
|
||
theorem mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 :=
|
||
division_ring.mul_inv_cancel H
|
||
|
||
theorem inv_mul_cancel (H : a ≠ 0) : a⁻¹ * a = 1 :=
|
||
division_ring.inv_mul_cancel H
|
||
|
||
theorem inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹
|
||
|
||
theorem div_eq_mul_one_div : a / b = a * (1 / b) :=
|
||
by rewrite [↑divide, one_mul]
|
||
|
||
theorem mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
|
||
by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]
|
||
|
||
theorem one_div_mul_cancel (H : a ≠ 0) : (1 / a) * a = 1 :=
|
||
by rewrite [-inv_eq_one_div, (inv_mul_cancel H)]
|
||
|
||
theorem div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H
|
||
|
||
theorem mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc
|
||
|
||
theorem one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 :=
|
||
assume H2 : 1 / a = 0,
|
||
have C1 : 0 = 1, from symm (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]),
|
||
absurd C1 zero_ne_one
|
||
|
||
-- the analogue in group is called inv_one
|
||
theorem inv_one_is_one : 1⁻¹ = 1 :=
|
||
by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))]
|
||
|
||
theorem div_one : a / 1 = a :=
|
||
by rewrite [↑divide, inv_one_is_one, mul_one]
|
||
|
||
theorem zero_div : 0 / a = 0 := !zero_mul
|
||
|
||
-- note: integral domain has a "mul_ne_zero". Discrete fields are int domains.
|
||
theorem mul_ne_zero' (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
|
||
assume H : a * b = 0,
|
||
have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
|
||
absurd C1 Ha
|
||
|
||
-- this belongs in ring?
|
||
theorem mul_ne_zero_imp_ne_zero (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
|
||
have Ha : a ≠ 0, from
|
||
(assume Ha1 : a = 0,
|
||
have H1 : a * b = 0, by rewrite [Ha1, zero_mul],
|
||
absurd H1 H),
|
||
have Hb : b ≠ 0, from
|
||
(assume Hb1 : b = 0,
|
||
have H1 : a * b = 0, by rewrite [Hb1, mul_zero],
|
||
absurd H1 H),
|
||
and.intro Ha Hb
|
||
|
||
theorem mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 :=
|
||
have H2 : a ≠ 0 ∧ b ≠ 0, from mul_ne_zero_imp_ne_zero H,
|
||
mul_ne_zero' (and.right H2) (and.left H2)
|
||
|
||
-- theorem inv_zero_imp_zero (H : a⁻¹ = 0) : a = 0 :=
|
||
-- classical?
|
||
|
||
-- make "left" and "right" versions?
|
||
theorem eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a :=
|
||
have H2 : a ≠ 0, from
|
||
(assume A : a = 0,
|
||
have B : 0 = 1, by rewrite [-(zero_mul b), -A, H],
|
||
absurd B zero_ne_one),
|
||
show b = 1 / a, from symm (calc
|
||
1 / a = (1 / a) * 1 : mul_one
|
||
... = (1 / a) * (a * b) : H
|
||
... = (1 / a) * a * b : mul.assoc
|
||
... = 1 * b : one_div_mul_cancel H2
|
||
... = b : one_mul)
|
||
|
||
-- which one is left and which is right?
|
||
theorem eq_one_div_of_mul_eq_one_left (H : b * a = 1) : b = 1 / a :=
|
||
have H2 : a ≠ 0, from
|
||
(assume A : a = 0,
|
||
have B : 0 = 1, from symm (calc
|
||
1 = b * a : symm H
|
||
... = b * 0 : A
|
||
... = 0 : mul_zero),
|
||
absurd B zero_ne_one),
|
||
show b = 1 / a, from symm (calc
|
||
1 / a = 1 * (1 / a) : one_mul
|
||
... = b * a * (1 / a) : H
|
||
... = b * (a * (1 / a)) : mul.assoc
|
||
... = b * 1 : mul_one_div_cancel H2
|
||
... = b : mul_one)
|
||
|
||
theorem one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) :=
|
||
have H : (b * a) * ((1 / a) * (1 / b)) = 1, by
|
||
rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)],
|
||
eq_one_div_of_mul_eq_one H
|
||
|
||
theorem one_div_neg_one_eq_neg_one : 1 / (-1) = -1 :=
|
||
have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg],
|
||
symm (eq_one_div_of_mul_eq_one H)
|
||
|
||
-- this should be in ring
|
||
theorem mul_neg_one_eq_neg : a * (-1) = -a :=
|
||
have H : a + a * -1 = 0, from calc
|
||
a + a * -1 = a * 1 + a * -1 : mul_one
|
||
... = a * (1 + -1) : left_distrib
|
||
... = a * 0 : add.right_inv
|
||
... = 0 : mul_zero,
|
||
symm (neg_eq_of_add_eq_zero H)
|
||
|
||
theorem one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) :=
|
||
have H1 : -1 ≠ 0, from
|
||
(assume H2 : -1 = 0, absurd (symm (calc
|
||
1 = -(-1) : neg_neg
|
||
... = -0 : H2
|
||
... = 0 : neg_zero)) zero_ne_one),
|
||
calc
|
||
1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul
|
||
... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1
|
||
... = (1 / a) * (-1) : one_div_neg_one_eq_neg_one
|
||
... = - (1 / a) : mul_neg_one_eq_neg
|
||
|
||
theorem div_neg_eq_neg_div (Ha : a ≠ 0) : b / (- a) = - (b / a) :=
|
||
calc
|
||
b / (- a) = b * (1 / (- a)) : inv_eq_one_div
|
||
... = b * -(1 / a) : one_div_neg_eq_neg_one_div Ha
|
||
... = -(b * (1 / a)) : neg_mul_eq_mul_neg
|
||
... = - (b * a⁻¹) : inv_eq_one_div
|
||
|
||
theorem neg_div (Ha : a ≠ 0) : (-b) / a = - (b / a) :=
|
||
by rewrite [neg_eq_neg_one_mul, mul_div_assoc, -neg_eq_neg_one_mul]
|
||
|
||
theorem neg_div_neg_eq_div (Hb : b ≠ 0) : (-a) / (-b) = a / b :=
|
||
by rewrite [(div_neg_eq_neg_div Hb), (neg_div Hb), neg_neg]
|
||
|
||
theorem div_div (H : a ≠ 0) : 1 / (1 / a) = a :=
|
||
symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel H))
|
||
|
||
theorem eq_of_invs_eq (Ha : a ≠ 0) (Hb : b ≠ 0) (H : 1 / a = 1 / b) : a = b :=
|
||
by rewrite [-(div_div Ha), H, (div_div Hb)]
|
||
|
||
-- oops, the analogous theorem in group is called inv_mul, but it *should* be called
|
||
-- mul_inv, in which case, we will have to rename this one
|
||
theorem mul_inv (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ :=
|
||
have H1 : b * a ≠ 0, from mul_ne_zero' Hb Ha,
|
||
eq.symm (calc
|
||
a⁻¹ * b⁻¹ = (1 / a) * b⁻¹ : inv_eq_one_div
|
||
... = (1 / a) * (1 / b) : inv_eq_one_div
|
||
... = (1 / (b * a)) : one_div_mul_one_div Ha Hb
|
||
... = (b * a)⁻¹ : inv_eq_one_div)
|
||
|
||
theorem mul_div_cancel (Hb : b ≠ 0) : a * b / b = a :=
|
||
by rewrite [↑divide, mul.assoc, (mul_inv_cancel Hb), mul_one]
|
||
|
||
theorem div_mul_cancel (Hb : b ≠ 0) : a / b * b = a :=
|
||
by rewrite [↑divide, mul.assoc, (inv_mul_cancel Hb), mul_one]
|
||
|
||
theorem div_add_div_same : a / c + b / c = (a + b) / c := !right_distrib⁻¹
|
||
|
||
theorem inv_mul_add_mul_inv_eq_inv_add_inv (Ha : a ≠ 0) (Hb : b ≠ 0) :
|
||
(1 / a) * (a + b) * (1 / b) = 1 / a + 1 / b :=
|
||
by rewrite [(left_distrib (1 / a)), (one_div_mul_cancel Ha), right_distrib, one_mul,
|
||
mul.assoc, (mul_one_div_cancel Hb), mul_one, add.comm]
|
||
|
||
theorem inv_mul_sub_mul_inv_eq_inv_add_inv (Ha : a ≠ 0) (Hb : b ≠ 0) :
|
||
(1 / a) * (b - a) * (1 / b) = 1 / a - 1 / b :=
|
||
by rewrite [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel Ha), mul_sub_right_distrib,
|
||
one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one, one_mul]
|
||
|
||
theorem div_eq_one_iff_eq (Hb : b ≠ 0) : a / b = 1 ↔ a = b :=
|
||
iff.intro
|
||
(assume H1 : a / b = 1, symm (calc
|
||
b = 1 * b : one_mul
|
||
... = a / b * b : H1
|
||
... = a : div_mul_cancel Hb))
|
||
(assume H2 : a = b, calc
|
||
a / b = b / b : H2
|
||
... = 1 : div_self Hb)
|
||
|
||
theorem eq_div_iff_mul_eq (Hc : c ≠ 0) : a = b / c ↔ a * c = b :=
|
||
iff.intro
|
||
(assume H : a = b / c, by rewrite [H, (div_mul_cancel Hc)])
|
||
(assume H : a * c = b, by rewrite [-(mul_div_cancel Hc), H])
|
||
|
||
theorem add_div_eq_mul_add_div (Hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
|
||
have H : (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)],
|
||
(iff.elim_right (eq_div_iff_mul_eq Hc)) H
|
||
|
||
-- There are many similar rules to these last two in the Isabelle library
|
||
-- that haven't been ported yet. Do as necessary.
|
||
|
||
end division_ring
|
||
|
||
structure field [class] (A : Type) extends division_ring A, comm_ring A
|
||
|
||
section field
|
||
variables [s : field A] {a b c d: A}
|
||
include s
|
||
local attribute divide [reducible]
|
||
|
||
theorem one_div_mul_one_div' (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (a * b) :=
|
||
by rewrite [(one_div_mul_one_div Ha Hb), mul.comm b]
|
||
|
||
theorem div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b :=
|
||
let Ha : a ≠ 0 := and.left (mul_ne_zero_imp_ne_zero H) in
|
||
symm (calc
|
||
1 / b = 1 * (1 / b) : one_mul
|
||
... = (a * a⁻¹) * (1 / b) : mul_inv_cancel Ha
|
||
... = a * (a⁻¹ * (1 / b)) : mul.assoc
|
||
... = a * ((1 / a) * (1 / b)) :inv_eq_one_div
|
||
... = a * (1 / (b * a)) : one_div_mul_one_div Ha Hb
|
||
... = a * (1 / (a * b)) : mul.comm
|
||
... = a * (a * b)⁻¹ : inv_eq_one_div)
|
||
|
||
theorem div_mul_left (Ha : a ≠ 0) (H : a * b ≠ 0) : b / (a * b) = 1 / a :=
|
||
let H1 : b * a ≠ 0 := mul_ne_zero_comm H in
|
||
by rewrite [mul.comm a, (div_mul_right Ha H1)]
|
||
|
||
theorem mul_div_cancel_left (Ha : a ≠ 0) : a * b / a = b :=
|
||
by rewrite [mul.comm a, (mul_div_cancel Ha)]
|
||
|
||
theorem mul_div_cancel' (Hb : b ≠ 0) : b * (a / b) = a :=
|
||
by rewrite [mul.comm, (div_mul_cancel Hb)]
|
||
|
||
theorem one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
|
||
have H [visible] : a * b ≠ 0, from (mul_ne_zero' Ha Hb),
|
||
by rewrite [add.comm, -(div_mul_left Ha H), -(div_mul_right Hb H), ↑divide, -right_distrib]
|
||
|
||
theorem div_mul_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) :=
|
||
by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv Hd Hb)]
|
||
|
||
theorem mul_div_mul_left (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b :=
|
||
have H [visible] : c * b ≠ 0, from mul_ne_zero' Hc Hb,
|
||
by rewrite [-(div_mul_div Hc Hb), (div_self Hc), one_mul]
|
||
|
||
theorem mul_div_mul_right (Hb : b ≠ 0) (Hc : c ≠ 0) : (a * c) / (b * c) = a / b :=
|
||
by rewrite [(mul.comm a), (mul.comm b), (mul_div_mul_left Hb Hc)]
|
||
|
||
theorem div_mul_eq_mul_div (Hc : c ≠ 0) : (b / c) * a = (b * a) / c :=
|
||
by rewrite [↑divide, mul.assoc, (mul.comm c⁻¹), -mul.assoc]
|
||
|
||
-- this one is odd -- I am not sure what to call it, but again, the prefix is right
|
||
theorem div_mul_eq_mul_div_comm (Hc : c ≠ 0) : (b / c) * a = b * (a / c) :=
|
||
by rewrite [(div_mul_eq_mul_div Hc), -(one_mul c), -(div_mul_div (ne.symm zero_ne_one) Hc), div_one, one_mul]
|
||
|
||
theorem div_add_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||
(a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
|
||
have H [visible] : b * d ≠ 0, from mul_ne_zero' Hb Hd,
|
||
by rewrite [-(mul_div_mul_right Hb Hd), -(mul_div_mul_left Hd Hb), div_add_div_same]
|
||
|
||
theorem div_sub_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
|
||
(a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
|
||
by rewrite [↑sub, neg_eq_neg_one_mul, -mul_div_assoc, (div_add_div Hb Hd),
|
||
-mul.assoc, (mul.comm b), mul.assoc, -neg_eq_neg_one_mul]
|
||
|
||
theorem mul_eq_mul_of_div_eq_div (Hb : b ≠ 0) (Hd : d ≠ 0) (H : a / b = c / d) : a * d = c * b :=
|
||
by rewrite [-mul_one, mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
|
||
-(div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div Hd), (div_mul_cancel Hd)]
|
||
|
||
theorem one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
|
||
have H : (a / b) * (b / a) = 1, from calc
|
||
(a / b) * (b / a) = (a * b) / (b * a) : div_mul_div Hb Ha
|
||
... = (a * b) / (a * b) : mul.comm
|
||
... = 1 : div_self (mul_ne_zero' Ha Hb),
|
||
symm (eq_one_div_of_mul_eq_one H)
|
||
|
||
theorem div_div_eq_mul_div (Hb : b ≠ 0) (Hc : c ≠ 0) : a / (b / c) = (a * c) / b :=
|
||
by rewrite [div_eq_mul_one_div, (one_div_div Hb Hc), -mul_div_assoc]
|
||
|
||
theorem div_div_eq_div_mul (Hb : b ≠ 0) (Hc : c ≠ 0) : (a / b) / c = a / (b * c) :=
|
||
by rewrite [div_eq_mul_one_div, (div_mul_div Hb Hc), mul_one]
|
||
|
||
theorem div_div_div_div (Hb : b ≠ 0) (Hc : c ≠ 0) (Hd : d ≠ 0) : (a / b) / (c / d) = (a * d) / (b * c) :=
|
||
by rewrite [(div_div_eq_mul_div Hc Hd), (div_mul_eq_mul_div Hb), (div_div_eq_div_mul Hb Hc)]
|
||
|
||
-- remaining to transfer from Isabelle fields: ordered fields
|
||
|
||
end field
|
||
|
||
structure discrete_field [class] (A : Type) extends field A :=
|
||
(decidable_equality : ∀x y : A, decidable (x = y))
|
||
|
||
section discrete_field
|
||
variable [s : discrete_field A]
|
||
include s
|
||
variables {a b c : A}
|
||
|
||
definition decidable_eq [instance] (a b : A) : decidable (a = b) :=
|
||
@discrete_field.decidable_equality A s a b
|
||
|
||
theorem discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero
|
||
(x y : A) (H : x * y = 0) : x = 0 ∨ y = 0 :=
|
||
decidable.by_cases
|
||
(assume H : x = 0, or.inl H)
|
||
(assume H1 : x ≠ 0,
|
||
or.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero]))
|
||
|
||
definition discrete_field.to_integral_domain [instance] [reducible] [coercion] :
|
||
integral_domain A :=
|
||
⦃ integral_domain, s,
|
||
eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
|
||
|
||
example (H1 : a ≠ 0) (H2 : b ≠ 0) : a * b ≠ 0 :=
|
||
@mul_ne_zero A s a b H1 H2
|
||
|
||
theorem inv_zero_imp_zero (H : 1 / a = 0) : a = 0 :=
|
||
decidable.by_cases
|
||
(assume Ha : a = 0, Ha)
|
||
(assume Ha: a ≠ 0, false.elim ((one_div_ne_zero Ha) H))
|
||
|
||
end discrete_field
|
||
|
||
end algebra
|