lean2/library/algebra/field.lean

343 lines
14 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
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