map_apply

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.map_apply

English

For any f and hf and valuation v, the value of the mapped valuation at r is f(v(r)).

Русский

Для любых f, hf и оценки v, значение отображаемой оценки в r равно f(v(r)).

LaTeX

$$$v.map\ f\ hf\ r = f(v\\, r)$$$

Lean4

@[simp]
theorem map_apply (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (v : Valuation R Γ₀) (r : R) : v.map f hf r = f (v r) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru