Theorems · Theorem · commutative algebra
false_of_nontrivial_of_product_domain
∀ (R : Type u_6) (S : Type u_7) [inst : Semiring R] [inst_1 : Semiring S] [IsDomain (R × S)] [Nontrivial R] [Nontrivial S], False
The product of two nontrivial rings is not a domain
- Defined in
- Mathlib.Algebra.Ring.Prod
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- mul_oneproof · cited by 3,885
- Nontrivialstatement and proof · cited by 2,416
- IsDomainstatement and proof · cited by 2,196
- MulZeroClass.mul_zeroproof · cited by 2,091
- zero_ne_oneproof · cited by 90
- NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zeroproof · cited by 14
- Prod.mk_eq_zeroproof · cited by 9
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.