Theorems · Theorem · commutative algebra

Valuation.IsEquiv.isNontrivial_iff

∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v : Valuation R Γ₀} {v' : Valuation R Γ'₀},
  v.IsEquiv v' → (v.IsNontrivial ↔ v'.IsNontrivial)

Defined in: Mathlib.RingTheory.Valuation.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 27 from the axioms · uses propext
Assumes: Ring LinearOrderedCommMonoidWithZero LinearOrderedCommMonoidWithZero

Mathlib docs Source Loogle LeanSearch

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
Valuationstatement and proof · cited by 823
LinearOrderedCommMonoidWithZerostatement and proof · cited by 139
Valuation.IsEquivstatement and proof · cited by 67
Valuation.IsNontrivialstatement and proof · cited by 27
Valuation.IsEquiv.symmproof · cited by 7
Valuation.isNontrivial_of_isEquivproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Valuation.isNontrivial_valuation_valuationSubring_iffproof · cited by 0