Theorems · Theorem · commutative algebra
ValuativeRel.isRankLeOne_iff_mulArchimedean
∀ {R : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R],
ValuativeRel.IsRankLeOne R ↔ MulArchimedean (ValuativeRel.ValueGroupWithZero R)- Defined in
- Mathlib.RingTheory.Valuation.RankOne
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingValuativeRel
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites28
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Ringstatement and proof · cited by 7,463
- NNRealproof · cited by 4,310
- LT.lt.ne'proof · cited by 1,417
- eq_or_neproof · cited by 1,117
- StrictMonoproof · cited by 706
- MonoidWithZeroHomproof · cited by 704
- zero_lt_oneproof · cited by 598
- ValuativeRelstatement and proof · cited by 241
- MonoidWithZeroHom.ofClassproof · cited by 204
- MonoidWithZeroHom.ValueGroup₀proof · cited by 166
- ValuativeRel.ValueGroupWithZerostatement and proof · cited by 86
Cited by1
Results whose statement or proof uses this declaration.
- ValuativeRel.IsRankLeOne.of_compatible_mulArchimedeanproof · cited by 1