WithValScalars.lean

instance uniformContinuousConstSMul (v : Valuation K Γ) :
    UniformContinuousConstSMul K (WithVal v) where
  uniformContinuous_const_smul k := by
    change UniformContinuous (fun x : WithVal v => toVal v k * x)
    exact uniformContinuous_mul_left' _

theorem uniformContinuousConstSMul_algebra {R : Type*} [CommSemiring R]
    [Algebra R K] (v : Valuation K Γ) :
    UniformContinuousConstSMul R (WithVal v) where
  uniformContinuous_const_smul r := by
    have heq : (fun x : WithVal v => r • x) =
        (fun x => WithVal.toVal v (algebraMap R K r) * x) := by
      funext x
      apply WithVal.ofVal_injective v
      exact Algebra.smul_def r x.ofVal
    rw [heq]
    exact uniformContinuous_mul_left' _

theorem denseRange_algebraMap_completion {R : Type*} [CommRing R] (v : Valuation R Γ) :
    DenseRange (algebraMap R v.Completion)