feat(library/algebra/group): add ordered semigroups
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
5daff18017
commit
4420f0dc0c
4 changed files with 317 additions and 32 deletions
|
|
@ -116,7 +116,6 @@ theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
|
|||
a + b = c + b → a = c :=
|
||||
!add_right_cancel_semigroup.add_right_cancel
|
||||
|
||||
|
||||
/- monoid -/
|
||||
|
||||
structure monoid [class] (A : Type) extends semigroup A, has_one A :=
|
||||
|
|
|
|||
|
|
@ -45,6 +45,23 @@ notation a >= b := has_le.ge a b
|
|||
definition has_lt.gt {A : Type} [s : has_lt A] (a b : A) := b < a
|
||||
notation a > b := has_lt.gt a b
|
||||
|
||||
theorem eq_le_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≤ c) :
|
||||
a ≤ c := H1⁻¹ ▸ H2
|
||||
|
||||
theorem le_eq_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a ≤ b) (H2 : b = c) :
|
||||
a ≤ c := H2 ▸ H1
|
||||
|
||||
theorem eq_lt_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b < c) :
|
||||
a < c := H1⁻¹ ▸ H2
|
||||
|
||||
theorem lt_eq_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a < b) (H2 : b = c) :
|
||||
a < c := H2 ▸ H1
|
||||
|
||||
calc_trans eq_le_trans
|
||||
calc_trans le_eq_trans
|
||||
calc_trans eq_lt_trans
|
||||
calc_trans lt_eq_trans
|
||||
|
||||
|
||||
/- weak orders -/
|
||||
|
||||
|
|
@ -57,6 +74,8 @@ theorem le_refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
|
|||
|
||||
theorem le_trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
|
||||
|
||||
calc_trans le_trans
|
||||
|
||||
theorem le_antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
|
||||
|
||||
structure linear_weak_order [class] (A : Type) extends weak_order A :=
|
||||
|
|
@ -76,15 +95,18 @@ theorem lt_irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_ir
|
|||
|
||||
theorem lt_trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
|
||||
|
||||
calc_trans lt_trans
|
||||
|
||||
theorem lt_imp_ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
|
||||
assume lt_ab : a < b, assume eq_ab : a = b, lt_irrefl a (eq_ab⁻¹ ▸ lt_ab)
|
||||
|
||||
|
||||
/- well-founded orders -/
|
||||
|
||||
structure wf_strict_order [class] (A : Type) extends strict_order A :=
|
||||
(wf_rec : ∀P : A → Type, (∀x, (∀y, lt y x → P y) → P x) → ∀x, P x)
|
||||
|
||||
-- TODO: is there a way to make this type check without specifying universe parameters?
|
||||
-- The good news is that the error message was very helpful.
|
||||
theorem wf_rec_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u v} A] {P : A → Type.{v}}
|
||||
definition wf_rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
|
||||
(x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
|
||||
wf_strict_order.wf_rec P H x
|
||||
|
||||
|
|
@ -152,6 +174,9 @@ have ne_ac : a ≠ c, from
|
|||
show false, from lt_imp_ne lt_bc eq_bc,
|
||||
show a < c, from le_ne_imp_lt le_ac ne_ac
|
||||
|
||||
calc_trans le_lt_trans
|
||||
calc_trans lt_le_trans
|
||||
|
||||
structure strong_order_pair [class] (A : Type) extends strict_order A, has_le A :=
|
||||
(le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
|
||||
|
||||
|
|
@ -161,7 +186,7 @@ theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b
|
|||
theorem le_imp_lt_or_eq [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
|
||||
iff.mp le_iff_lt_or_eq le_ab
|
||||
|
||||
theorem strong_order_pair.to_order_pair [instance] [s : strong_order_pair A] : order_pair A :=
|
||||
definition strong_order_pair.to_order_pair [instance] [s : strong_order_pair A] : order_pair A :=
|
||||
order_pair.mk
|
||||
strong_order_pair.le
|
||||
(take a, show a ≤ a, from iff.mp (iff.symm le_iff_lt_or_eq) (or.intro_right _ rfl))
|
||||
|
|
@ -203,4 +228,3 @@ structure linear_strong_order_pair (A : Type) extends strong_order_pair A :=
|
|||
(trichotomy : ∀a b, lt a b ∨ a = b ∨ lt b a)
|
||||
|
||||
end algebra
|
||||
|
||||
|
|
|
|||
174
library/algebra/ordered_group.lean
Normal file
174
library/algebra/ordered_group.lean
Normal file
|
|
@ -0,0 +1,174 @@
|
|||
/-
|
||||
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Module: algebra.ordered_group
|
||||
Authors: Jeremy Avigad
|
||||
|
||||
Partially ordered additive groups. Modeled on Isabelle's library. The comments below indicate that
|
||||
we could refine the structures, though we would have to declare more inheritance paths.
|
||||
-/
|
||||
|
||||
import logic.eq logic.connectives
|
||||
import data.unit data.sigma data.prod
|
||||
import algebra.function algebra.binary
|
||||
import algebra.group algebra.order
|
||||
|
||||
open eq eq.ops -- note: ⁻¹ will be overloaded
|
||||
|
||||
namespace algebra
|
||||
|
||||
variable {A : Type}
|
||||
|
||||
structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A,
|
||||
add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A :=
|
||||
(add_le_left : ∀a b c, le a b → le (add c a) (add c b))
|
||||
(add_le_left_cancel : ∀a b c, le (add c a) (add c b) → le a b)
|
||||
|
||||
section
|
||||
|
||||
variables [s : ordered_cancel_comm_monoid A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
theorem add_le_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
|
||||
!ordered_cancel_comm_monoid.add_le_left H
|
||||
|
||||
theorem add_le_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + c :=
|
||||
(add_comm c a) ▸ (add_comm c b) ▸ (add_le_left H c)
|
||||
|
||||
theorem add_le {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
|
||||
le_trans (add_le_right Hab c) (add_le_left Hcd b)
|
||||
|
||||
theorem add_lt_left {a b : A} (H : a < b) (c : A) : c + a < c + b :=
|
||||
have H1 : c + a ≤ c + b, from add_le_left (lt_imp_le H) c,
|
||||
have H2 : c + a ≠ c + b, from
|
||||
take H3 : c + a = c + b,
|
||||
have H4 : a = b, from add_left_cancel H3,
|
||||
lt_imp_ne H H4,
|
||||
le_ne_imp_lt H1 H2
|
||||
|
||||
theorem add_lt_right {a b : A} (H : a < b) (c : A) : a + c < b + c :=
|
||||
(add_comm c a) ▸ (add_comm c b) ▸ (add_lt_left H c)
|
||||
|
||||
theorem add_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
|
||||
lt_trans (add_lt_right Hab c) (add_lt_left Hcd b)
|
||||
|
||||
theorem add_le_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
|
||||
le_lt_trans (add_le_right Hab c) (add_lt_left Hcd b)
|
||||
|
||||
theorem add_lt_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
|
||||
lt_le_trans (add_lt_right Hab c) (add_le_left Hcd b)
|
||||
|
||||
-- here we start using add_le_left_cancel.
|
||||
theorem add_le_left_cancel {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
|
||||
!ordered_cancel_comm_monoid.add_le_left_cancel H
|
||||
|
||||
theorem add_le_right_cancel {a b c : A} (H : a + b ≤ c + b) : a ≤ c :=
|
||||
add_le_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
|
||||
|
||||
theorem add_lt_left_cancel {a b c : A} (H : a + b < a + c) : b < c :=
|
||||
have H1 : b ≤ c, from add_le_left_cancel (lt_imp_le H),
|
||||
have H2 : b ≠ c, from
|
||||
assume H3 : b = c, lt_irrefl _ (H3 ▸ H),
|
||||
le_ne_imp_lt H1 H2
|
||||
|
||||
theorem add_lt_right_cancel {a b c : A} (H : a + b < c + b) : a < c :=
|
||||
add_lt_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
|
||||
|
||||
theorem add_le_left_iff : a + b ≤ a + c ↔ b ≤ c :=
|
||||
iff.intro add_le_left_cancel (assume H, add_le_left H _)
|
||||
|
||||
theorem add_le_right_iff : a + b ≤ c + b ↔ a ≤ c :=
|
||||
iff.intro add_le_right_cancel (assume H, add_le_right H _)
|
||||
|
||||
theorem add_lt_left_iff : a + b < a + c ↔ b < c :=
|
||||
iff.intro add_lt_left_cancel (assume H, add_lt_left H _)
|
||||
|
||||
theorem add_lt_right_iff : a + b < c + b ↔ a < c :=
|
||||
iff.intro add_lt_right_cancel (assume H, add_lt_right H _)
|
||||
|
||||
-- here we start using properties of zero.
|
||||
theorem add_nonneg_nonneg {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
|
||||
!add_left_id ▸ (add_le Ha Hb)
|
||||
|
||||
theorem add_pos_nonneg {a b : A} (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
|
||||
!add_left_id ▸ (add_lt_le Ha Hb)
|
||||
|
||||
theorem add_nonneg_pos {a b : A} (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
|
||||
!add_left_id ▸ (add_le_lt Ha Hb)
|
||||
|
||||
theorem add_pos_pos {a b : A} (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
|
||||
!add_left_id ▸ (add_lt Ha Hb)
|
||||
|
||||
theorem add_nonpos_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
|
||||
!add_left_id ▸ (add_le Ha Hb)
|
||||
calc_trans le_eq_trans
|
||||
|
||||
theorem add_neg_nonpos {a b : A} (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
|
||||
!add_left_id ▸ (add_lt_le Ha Hb)
|
||||
|
||||
theorem add_nonpos_neg {a b : A} (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
|
||||
!add_left_id ▸ (add_le_lt Ha Hb)
|
||||
|
||||
theorem add_neg_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
|
||||
!add_left_id ▸ (add_lt Ha Hb)
|
||||
|
||||
-- TODO: add nonpos version (will be easier with simplifier)
|
||||
theorem add_nonneg_eq_zero_iff {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
|
||||
iff.intro
|
||||
(assume Hab : a + b = 0,
|
||||
have Ha' : a ≤ 0, from
|
||||
calc
|
||||
a = a + 0 : add_right_id
|
||||
... ≤ a + b : add_le_left Hb
|
||||
... = 0 : Hab,
|
||||
have Haz : a = 0, from le_antisym Ha' Ha,
|
||||
have Hb' : b ≤ 0, from
|
||||
calc
|
||||
b = 0 + b : add_left_id
|
||||
... ≤ a + b : add_le_right Ha
|
||||
... = 0 : Hab,
|
||||
have Hbz : b = 0, from le_antisym Hb' Hb,
|
||||
and.intro Haz Hbz)
|
||||
(assume Hab : a = 0 ∧ b = 0,
|
||||
(and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_right_id 0))
|
||||
|
||||
theorem le_add_nonneg (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c := !add_left_id ▸ add_le Ha Hbc
|
||||
theorem le_nonneg_add (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ c + a := !add_right_id ▸ add_le Hbc Ha
|
||||
theorem le_add_pos (Ha : 0 < a) (Hbc : b ≤ c) : b < a + c := !add_left_id ▸ add_lt_le Ha Hbc
|
||||
theorem le_pos_add (Ha : 0 < a) (Hbc : b ≤ c) : b < c + a := !add_right_id ▸ add_le_lt Hbc Ha
|
||||
theorem le_add_nonpos (Ha : a ≤ 0) (Hbc : b ≤ c) : a + b ≤ c := !add_left_id ▸ add_le Ha Hbc
|
||||
theorem le_nonpos_add (Ha : a ≤ 0) (Hbc : b ≤ c) : b + a ≤ c := !add_right_id ▸ add_le Hbc Ha
|
||||
theorem le_add_neg (Ha : a < 0) (Hbc : b ≤ c) : a + b < c := !add_left_id ▸ add_lt_le Ha Hbc
|
||||
theorem le_neg_add (Ha : a < 0) (Hbc : b ≤ c) : b + a < c := !add_right_id ▸ add_le_lt Hbc Ha
|
||||
theorem lt_add_nonneg (Ha : 0 ≤ a) (Hbc : b < c) : b < a + c := !add_left_id ▸ add_le_lt Ha Hbc
|
||||
theorem lt_nonneg_add (Ha : 0 ≤ a) (Hbc : b < c) : b < c + a := !add_right_id ▸ add_lt_le Hbc Ha
|
||||
theorem lt_add_pos (Ha : 0 < a) (Hbc : b < c) : b < a + c := !add_left_id ▸ add_lt Ha Hbc
|
||||
theorem lt_pos_add (Ha : 0 < a) (Hbc : b < c) : b < c + a := !add_right_id ▸ add_lt Hbc Ha
|
||||
theorem lt_add_nonpos (Ha : a ≤ 0) (Hbc : b < c) : a + b < c := !add_left_id ▸ add_le_lt Ha Hbc
|
||||
theorem lt_nonpos_add (Ha : a ≤ 0) (Hbc : b < c) : b + a < c := !add_right_id ▸ add_lt_le Hbc Ha
|
||||
theorem lt_add_neg (Ha : a < 0) (Hbc : b < c) : a + b < c := !add_left_id ▸ add_lt Ha Hbc
|
||||
theorem lt_neg_add (Ha : a < 0) (Hbc : b < c) : b + a < c := !add_right_id ▸ add_lt Hbc Ha
|
||||
end
|
||||
|
||||
-- TODO: there is more we can do if we have max and min (in order.lean as well)
|
||||
|
||||
-- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b, but it is not clear whether
|
||||
-- this gives us any useful generality
|
||||
|
||||
structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
|
||||
(add_le_left : ∀a b c, le a b → le (add c a) (add c b))
|
||||
|
||||
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
|
||||
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
|
||||
ordered_cancel_comm_monoid.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm
|
||||
(@add_left_cancel _ _) (@add_right_cancel _ _) has_le.le le_refl (@le_trans _ _) (@le_antisym _ _)
|
||||
has_lt.lt (@lt_iff_le_ne _ _) ordered_comm_group.add_le_left
|
||||
proof
|
||||
take a b c : A,
|
||||
assume H : c + a ≤ c + b,
|
||||
have H' : -c + (c + a) ≤ -c + (c + b), from ordered_comm_group.add_le_left _ _ _ H,
|
||||
!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
|
||||
qed
|
||||
|
||||
end algebra
|
||||
|
|
@ -172,34 +172,74 @@ semiring.mk ring.add ring.add_assoc ring.zero ring.add_left_id
|
|||
|
||||
section
|
||||
|
||||
variables [s : ring A] (a b c : A)
|
||||
variables [s : ring A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
theorem neg_mul_left : -(a * b) = (-a) * b :=
|
||||
theorem neg_mul_left : -(a * b) = -a * b :=
|
||||
neg_unique
|
||||
(calc
|
||||
a * b + (-a) * b = (a + -a) * b : distrib_right
|
||||
a * b + -a * b = (a + -a) * b : distrib_right
|
||||
... = 0 * b : add_right_inv
|
||||
... = 0 : mul_zero_left)
|
||||
|
||||
theorem neg_mul_right : -(a * b) = a * (-b) :=
|
||||
theorem neg_mul_right : -(a * b) = a * -b :=
|
||||
neg_unique
|
||||
(calc
|
||||
a * b + a * (-b) = a * (b + -b) : distrib_left
|
||||
a * b + a * -b = a * (b + -b) : distrib_left
|
||||
... = a * 0 : add_right_inv
|
||||
... = 0 : mul_zero_right)
|
||||
|
||||
theorem neg_mul_neg : (-a) * (-b) = a * b :=
|
||||
theorem neg_mul_neg : -a * -b = a * b :=
|
||||
calc
|
||||
(-a) * (-b) = -(a * -b) : neg_mul_left
|
||||
-a * -b = -(a * -b) : neg_mul_left
|
||||
... = - -(a * b) : neg_mul_right
|
||||
... = a * b : neg_neg
|
||||
|
||||
theorem neg_mul_comm : -a * b = a * -b := !neg_mul_left⁻¹ ⬝ !neg_mul_right
|
||||
|
||||
theorem minus_distrib_left : a * (b - c) = a * b - a * c :=
|
||||
calc
|
||||
a * (b - c) = a * b + a * -c : distrib_left
|
||||
... = a * b + - (a * c) : neg_mul_right
|
||||
... = a * b - a * c : rfl
|
||||
|
||||
theorem minus_distrib_right : (a - b) * c = a * c - b * c :=
|
||||
calc
|
||||
(a - b) * c = a * c + -b * c : distrib_right
|
||||
... = a * c + - (b * c) : neg_mul_left
|
||||
... = a * c - b * c : rfl
|
||||
|
||||
-- TODO: can calc mode be improved to make this easier?
|
||||
-- TODO: there is also the other direction. It will be easier when we
|
||||
-- have the simplifier.
|
||||
theorem eq_add_iff1 : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
|
||||
calc
|
||||
a * e + c = b * e + d ↔ a * e + c = d + b * e : !add_comm ▸ !iff.refl
|
||||
... ↔ a * e + c - b * e = d : iff.symm !minus_eq_iff_eq_add
|
||||
... ↔ a * e - b * e + c = d : !minus_add_right_comm ▸ !iff.refl
|
||||
... ↔ (a - b) * e + c = d : !minus_distrib_right ▸ !iff.refl
|
||||
|
||||
end
|
||||
|
||||
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
|
||||
|
||||
/- TODO: show a comm_ring is a comm-semiring -/
|
||||
definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
|
||||
comm_semiring.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm
|
||||
has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right
|
||||
mul_zero_left mul_zero_right zero_ne_one mul_comm
|
||||
|
||||
section
|
||||
|
||||
variables [s : comm_ring A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
-- TODO: wait for the simplifier
|
||||
theorem square_minus_square_eq : a * a - b * b = (a + b) * (a - b) := sorry
|
||||
|
||||
theorem square_minus_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
|
||||
!mul_right_id ▸ !square_minus_square_eq
|
||||
|
||||
end
|
||||
|
||||
structure comm_ring_dvd [class] (A : Type) extends comm_ring A, has_dvd A
|
||||
|
||||
|
|
@ -208,4 +248,52 @@ comm_semiring_dvd.mk has_add.add add_assoc has_zero.zero add_left_id add_right_i
|
|||
has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right
|
||||
mul_zero_left mul_zero_right zero_ne_one mul_comm dvd (@dvd_intro A s) (@dvd_imp_exists A s)
|
||||
|
||||
section
|
||||
|
||||
variables [s : comm_ring_dvd A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
theorem dvd_neg_iff : a | -b ↔ a | b :=
|
||||
iff.intro
|
||||
(assume H : a | -b,
|
||||
dvd_elim H
|
||||
(take c, assume H' : a * c = -b,
|
||||
dvd_intro
|
||||
(calc
|
||||
a * -c = -(a * c) : neg_mul_right
|
||||
... = -(-b) : H'
|
||||
... = b : neg_neg)))
|
||||
(assume H : a | b,
|
||||
dvd_elim H
|
||||
(take c, assume H' : a * c = b,
|
||||
dvd_intro
|
||||
(calc
|
||||
a * -c = -(a * c) : neg_mul_right
|
||||
... = -b : H')))
|
||||
|
||||
theorem neg_dvd_iff : -a | b ↔ a | b :=
|
||||
iff.intro
|
||||
(assume H : -a | b,
|
||||
dvd_elim H
|
||||
(take c, assume H' : -a * c = b,
|
||||
dvd_intro
|
||||
(calc
|
||||
a * -c = -a * c : neg_mul_comm
|
||||
... = b : H')))
|
||||
(assume H : a | b,
|
||||
dvd_elim H
|
||||
(take c, assume H' : a * c = b,
|
||||
dvd_intro
|
||||
(calc
|
||||
-a * -c = a * c : neg_mul_neg
|
||||
... = b : H')))
|
||||
|
||||
theorem dvd_diff (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=
|
||||
dvd_add H₁ (iff.elim_right !dvd_neg_iff H₂)
|
||||
|
||||
end
|
||||
|
||||
/- ring no_zero_divisors -/
|
||||
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
Loading…
Reference in a new issue