Theorems · Theorem · ring theory
isDomain_iff_noZeroDivisors_and_nontrivial
∀ (α : Type u_3) [inst : Ring α], IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
- Defined in
- Mathlib.Algebra.Ring.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Nontrivialstatement and proof · cited by 2,416
- IsDomainstatement and proof · cited by 2,196
- NoZeroDivisorsstatement · cited by 545
- IsCancelMulZeroproof · cited by 177
- isCancelMulZero_iff_noZeroDivisorsproof · cited by 2
- isDomain_iff_cancelMulZero_and_nontrivialproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- IsBaseChange.lift_rank_eqproof · cited by 3
- Algebra.IsAlgebraic.isDomain_of_adjoin_rangeproof · cited by 2
- IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_sdiffproof · cited by 2
- exists_isTranscendenceBasis_betweenproof · cited by 1
- AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasisproof · cited by 1
- IsAlgebraic.adjoin_of_forall_isAlgebraicproof · cited by 1
- Algebra.isAlgebraic_adjoin_of_nonemptyproof · cited by 1