instCommMonoidWithZeroSubtypeMemSubmonoidMrange

English

The image of a valuation is equipped with a natural commutative monoid with zero structure.

Русский

Образ валюации имеет естественную структуру коммутативного монома с нулём.

LaTeX

$$$ \\operatorname{CommMonoidWithZero}(\\operatorname{MonoidHom.mrange}(v)). $$$

Lean4

instance (v : Valuation R Γ₀) : CommMonoidWithZero (MonoidHom.mrange v) :=
  inferInstanceAs (CommMonoidWithZero (MonoidHom.mrange (v : R →*₀ Γ₀)))

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