extendToLocalization_mk' — Mathlib

English

A specialized form of extendToLocalization asserts a specific behavior on mk' elements: the extended valuation of mk' equals the product of the base valuation and the inverse of the valuation of the multiplier.

Русский

Уточнённая форма extendToLocalization утверждает, что для mk' элемент extended valuation равен произведению базовой оценки на обратную оценку множителя.

LaTeX

$$$ (v.extendToLocalization hS B) (IsLocalization.mk' B x y) = v x \\cdot (v y)^{-1} $$$

Lean4

@[simp]
theorem extendToLocalization_mk' (x : A) (y : S) :
    (v.extendToLocalization hS B) (IsLocalization.mk' _ x y) = v x * (v y)⁻¹ :=
  (Submonoid.LocalizationMap.lift_mk' _ _ _ _).trans (by simp [IsUnit.coe_liftRight])

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