Theorems · Theorem · commutative algebra
WithVal.equiv_symm_apply
∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
(ofVal : R), (WithVal.equiv v).symm ofVal = WithVal.toVal v ofVal- Defined in
- Mathlib.Topology.Algebra.Valued.WithVal
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses 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.coestatement and proof · cited by 62,936
- Ringstatement and proof · cited by 7,463
- RingEquivstatement · cited by 1,147
- Valuationstatement and proof · cited by 823
- RingEquiv.symmstatement and proof · cited by 567
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- WithValstatement · cited by 151
- WithVal.equivstatement and proof · cited by 36
Cited by13
Results whose statement or proof uses this declaration.
- NumberField.FinitePlace.norm_embeddingproof · cited by 6
- Valuation.IsEquiv.uniformContinuous_equivproof · cited by 2
- Valuation.IsEquiv.uniformContinuous_equiv_symmproof · cited by 1
- WithVal.equivWithVal_applyproof · cited by 0
- WithVal.equivWithVal_symm_applyproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_memproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_addproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mulproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_oneproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zeroproof · cited by 0
- LaurentSeries.tendsto_valuationproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coeproof · cited by 0