Theorems · Theorem · commutative algebra

Valuation.toUniformSpace_eq

∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible],
  _u = IsTopologicalAddGroup.rightUniformSpace R

Defined in: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Cited by: 2 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring ValuativeRel LinearOrderedCommGroupWithZero UniformSpace IsUniformAddGroup IsValuativeTopology Valuation.Compatible

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites42

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
Setproof · cited by 53,352
SetLike.coeproof · cited by 8,199
Filterproof · cited by 8,121
Ringstatement and proof · cited by 7,463
Set.ofPredproof · cited by 6,101
nhdsproof · cited by 5,554
Set.preimageproof · cited by 4,946
MonoidHomstatement · cited by 3,629
Subgroupstatement · cited by 3,593
Unitsstatement and proof · cited by 2,804
UniformSpacestatement and proof · cited by 2,040

Cited by2

Results whose statement or proof uses this declaration.

Valuation.cauchy_iffproof · cited by 0
Valuation.toTopologicalSpace_eqproof · cited by 0