extendToLocalization_apply_map_apply

English

The extendToLocalization respects the algebra map from A to B: applying the extended valuation to algebraMap(a) yields the original valuation of a.

Русский

Расширенная оценка сохраняет отображение по алгебраическому отображению: применение оценки к algebraMap(a) даёт исходную оценку a.

LaTeX

$$$ v.extendToLocalization hS B (algebraMap A B a) = v a $$$

Lean4

@[simp]
theorem extendToLocalization_apply_map_apply (a : A) : v.extendToLocalization hS B (algebraMap A B a) = v a :=
  Submonoid.LocalizationMap.lift_eq _ _ a

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