Theorems · Theorem · commutative algebra

ValuativeRel.nonempty_orderIso_withZeroMul_int_iff

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R],
  Nonempty (ValuativeRel.ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    ValuativeRel.IsDiscrete R ∧ ValuativeRel.IsNontrivial R ∧ MulArchimedean (ValuativeRel.ValueGroupWithZero R)

Defined in: Mathlib.RingTheory.Valuation.DiscreteValuativeRel
Cited by: 1 results in Mathlib
Foundations: Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring ValuativeRel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Semiringstatement and proof · cited by 13,802
eq_or_neproof · cited by 1,117
Multiplicativestatement and proof · cited by 875
LT.lt.neproof · cited by 872
map_oneproof · cited by 861
WithZerostatement and proof · cited by 586
DenselyOrderedproof · cited by 471
le_of_not_gtproof · cited by 430
LT.lt.not_geproof · cited by 305
ValuativeRelstatement and proof · cited by 241
neg_neg_of_posproof · cited by 227

Cited by1

Results whose statement or proof uses this declaration.

ValuativeRel.IsDiscrete.of_compatible_withZeroMulIntproof · cited by 0