mapOfLE_comp_valuation — Mathlib

English

For R ≤ S, composing the map R → S with the valuation on R equals the valuation on S; i.e., the valuation maps commute with the inclusion.

Русский

Пусть R ≤ S. Тогда композиция R → S с R-оценкой равна S-оценке; т.е. значения в S совпадают после включения.

LaTeX

$$$ (R.mapOfLE S\, h) \circ R.valuation = S.valuation $$$

Lean4

@[simp]
theorem mapOfLE_comp_valuation (R S : ValuationSubring K) (h : R ≤ S) : R.mapOfLE S h ∘ R.valuation = S.valuation := by
  ext; rfl

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