From 72c86c3f66b2688cbe5cdf7bd0bd8e5061a84cba Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 12 Jan 2022 07:31:04 +0000 Subject: [PATCH] chore(algebra/ring/basic): generalize `is_domain.to_cancel_monoid_with_zero` to `no_zero_divisors` (#11387) This generalization doesn't work for typeclass search as `cancel_monoid_with_zero` implies `no_zero_divisors` which would form a loop, but it can be useful for a `letI` in another proof. Independent of whether this turns out to be useful, it's nice to show that nontriviality doesn't affect the fact that rings with no zero divisors are cancellative. --- src/algebra/ring/basic.lean | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean index 3bcefc04e7fa5..30bd914c17467 100644 --- a/src/algebra/ring/basic.lean +++ b/src/algebra/ring/basic.lean @@ -1031,6 +1031,18 @@ lemma is_regular_of_ne_zero' [ring α] [no_zero_divisors α] {k : α} (hk : k is_right_regular_of_non_zero_divisor k (λ x h, (no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hk)⟩ +/-- A ring with no zero divisors is a cancel_monoid_with_zero. + +Note this is not an instance as it forms a typeclass loop. -/ +@[reducible] +def no_zero_divisors.to_cancel_monoid_with_zero [ring α] [no_zero_divisors α] : + cancel_monoid_with_zero α := +{ mul_left_cancel_of_ne_zero := λ a b c ha, + @is_regular.left _ _ _ (is_regular_of_ne_zero' ha) _ _, + mul_right_cancel_of_ne_zero := λ a b c hb, + @is_regular.right _ _ _ (is_regular_of_ne_zero' hb) _ _, + .. (infer_instance : semiring α) } + /-- A domain is a nontrivial ring with no zero divisors, i.e. satisfying the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. @@ -1046,11 +1058,7 @@ variables [ring α] [is_domain α] @[priority 100] -- see Note [lower instance priority] instance is_domain.to_cancel_monoid_with_zero : cancel_monoid_with_zero α := -{ mul_left_cancel_of_ne_zero := λ a b c ha, - @is_regular.left _ _ _ (is_regular_of_ne_zero' ha) _ _, - mul_right_cancel_of_ne_zero := λ a b c hb, - @is_regular.right _ _ _ (is_regular_of_ne_zero' hb) _ _, - .. (infer_instance : semiring α) } +no_zero_divisors.to_cancel_monoid_with_zero /-- Pullback an `is_domain` instance along an injective function. -/ protected theorem function.injective.is_domain [ring β] (f : β →+* α) (hf : injective f) :