Theorems · Theorem · commutative algebra
Valuation.map_div
∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_7} [inst_1 : DivisionRing R]
(v : Valuation R Γ₀) (x y : R), v (x / y) = v x / v y- Defined in
- Mathlib.RingTheory.Valuation.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- DivisionRingstatement and proof · cited by 1,062
- Valuationstatement and proof · cited by 823
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- map_div₀proof · cited by 98
Cited by3
Results whose statement or proof uses this declaration.
- Valuation.isEquiv_of_val_le_oneproof · cited by 3
- ValuativeRel.ValueGroupWithZero.mk_eq_valuationproof · cited by 1
- RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_Xproof · cited by 1