Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Valuation
variable {K Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)instance continuousConstSMul_withVal : ContinuousConstSMul K (WithVal v)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Valuation
variable {K Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)instance uniformContinuousConstSMul_withVal : UniformContinuousConstSMul K (WithVal v)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Valuation
variable {K Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)instance algebraCompletion : Algebra K v.CompletionSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Valuation
variable {K Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)theorem algebraMap_completion_apply (a : K) : algebraMap K v.Completion a = (a :
v.Completion)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace Valuation
variable {K Γ₀ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)theorem smul_completion_def (a : K) (x : v.Completion) : a • x = (a : v.Completion) * x