feat(ValuativeRel): instance IsLinearTopology 𝒪[K] 𝒪[K]

Author: WenrongZou

Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean

@@ -6,6 +6,7 @@ Authors: Jiedong Jiang
 module
 
 public import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
+public import Mathlib.Topology.Algebra.LinearTopology
 public import Mathlib.Topology.Algebra.Valued.ValuationTopology
 
 /-!
@@ -422,6 +423,16 @@ end Valuation
 
 namespace IsValuativeTopology
 
+/-- The topology on the ring of integers of a ring `R` carrying a valuative topology is linear:
+the open balls `Valuation.ltIdeal (valuation R) γ` form a basis of neighborhoods of zero
+made of ideals. -/
+instance [TopologicalSpace R] [IsValuativeTopology R] :
+    IsLinearTopology (valuation R).integer (valuation R).integer := by
+  refine IsLinearTopology.mk_of_hasBasis _
+    (p := fun _ : (ValueGroupWithZero R)ˣ ↦ True) (s := (valuation R).ltIdeal) ?_
+  rw [nhds_subtype_eq_comap]
+  exact (IsValuativeTopology.hasBasis_nhds_zero R).comap _
+
 @[deprecated (since := "2026-03-17")] alias isOpen_ball := Valuation.isOpen_ball
 @[deprecated (since := "2026-03-17")] alias isClosed_ball := Valuation.isClosed_ball
 @[deprecated (since := "2026-03-17")] alias isClopen_ball := Valuation.isClopen_ball