Theorems · Definition · commutative algebra
Valuation.toMonoidWithZeroHom
{R : Type u_3} →
{Γ₀ : Type u_4} → [inst : LinearOrderedCommMonoidWithZero Γ₀] → [inst_1 : Ring R] → Valuation R Γ₀ → R →*₀ Γ₀- Defined in
- Mathlib.RingTheory.Valuation.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- MonoidWithZeroHomstatement · cited by 704
- LinearOrderedCommMonoidWithZerostatement and proof · cited by 139
Cited by20
Results whose statement or proof uses this declaration.
- Valuation.map_oneproof · cited by 17
- ValuationSubring.unitGroupproof · cited by 16
- Valuation.comapproof · cited by 15
- Valuation.map_mulproof · cited by 13
- Valuation.map_negproof · cited by 11
- Valuation.map_zeroproof · cited by 11
- Valuation.map_sub_swapproof · cited by 7
- Valuation.mapproof · cited by 4
- Valuation.extendToLocalizationproof · cited by 4
- Valuation.map_powproof · cited by 4
- Valuation.map_add_le_max'statement · cited by 3
- Ring.ordFrac_eq_inverse_comp_valuationstatement and proof · cited by 2