mk_eq_div — Mathlib

English

For r ∈ R and s ∈ posSubmonoid R, ValueGroupWithZero.mk r s equals valuation R r divided by valuation R s.

Русский

Для r ∈ R и s ∈ posSubmonoid R, ValueGroupWithZero.mk r s равно отношению valuation R r к valuation R s.

LaTeX

$$$\mathrm{ValueGroupWithZero.mk} \, r \, s = \frac{\mathrm{valuation}(R,r)}{\mathrm{valuation}(R,s)}$$$

Lean4

theorem mk_eq_div (r : R) (s : posSubmonoid R) : ValueGroupWithZero.mk r s = valuation R r / valuation R (s : R) :=
  by
  rw [eq_div_iff (valuation_posSubmonoid_ne_zero _)]
  simp [valuation, mk_eq_mk]

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