Theorems · Definition · field theory
Valued.extensionValuation
{K : Type u_1} →
[inst : Field K] →
{Γ₀ : Type u_2} →
[inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [hv : Valued K Γ₀] → Valuation (UniformSpace.Completion K) Γ₀the extension of a valuation on a division ring to its completion.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- Valuationstatement · cited by 823
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- UniformSpace.Completionstatement and proof · cited by 192
- Valuedstatement and proof · cited by 70
- MonoidWithZeroHom.ValueGroup₀.embeddingproof · cited by 47
- Valued.extensionproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- Valued.extensionValuation_apply_coestatement · cited by 3
- Valued.closure_coe_completion_v_ltstatement and proof · cited by 1
- RatFunc.valuedCompletionAtInfty.defstatement · cited by 1
- Valued.extensionValuation_coe_applystatement · cited by 0
- Valued.extensionValuation_toFunstatement · cited by 0
- Valued.extension_eq_zero_iffproof · cited by 0
- FunctionField.valuedFqtInfty.defstatement · cited by 0
- Valued.closure_coe_completion_v_mul_v_ltstatement and proof · cited by 0
- Valued.valueGroup₀_equiv_extensionValuationstatement · cited by 0
- Valued.valueGroup₀_hom_extensionValuationstatement and proof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_defstatement · cited by 0
- Valued.exists_coe_eq_vstatement · cited by 0