instCompatibleValueGroupWithZeroV

English

The valuation v on K is compatible with the value group with zero structure, i.e., the induced value group is aligned with the valuation.

Русский

Оценка v на K совместима со структурой группы значений с нулём; индуцируемая группа значений согласована с оценкой.

LaTeX

$$$$v: K \to \Gamma_0 \text{ is compatible with the value group } \Gamma_0.$$$$

Lean4

instance (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsValuativeTopology K] :
    (Valued.v (R := K) (Γ₀ := ValueGroupWithZero K)).Compatible :=
  inferInstanceAs (valuation K).Compatible

Похожие утверждения