Theorems · Theorem · commutative algebra
Valuation.IsEquiv.uniformContinuous_equivWithVal
Deprecated since 2026-01-27Use Valuation.IsEquiv.uniformContinuous_congr instead.
∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
[inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'},
v.IsEquiv w → UniformContinuous ⇑(WithVal.congr v w (RingEquiv.refl R))Alias of Valuation.IsEquiv.uniformContinuous_congr.
- Defined in
- Mathlib.Topology.Algebra.Valued.WithVal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Ringstatement · cited by 7,463
- RingEquivstatement · cited by 1,147
- Valuationstatement · cited by 823
- LinearOrderedCommGroupWithZerostatement · cited by 528
- UniformContinuousstatement · cited by 410
- WithValstatement · cited by 151
- RingEquiv.reflstatement · cited by 72
- Valuation.IsEquivstatement · cited by 67
- WithVal.congrstatement · cited by 10
- Valuation.IsEquiv.uniformContinuous_congrproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.