ext

Mathlib.RingTheory.Valuation.Basic

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

English

Two valuations are equal if they agree on every ring element.

Русский

Две валюации равны, если они согласны на каждом элементе кольца.

LaTeX

$$$ (\forall r \in R, v_1(r) = v_2(r)) \Rightarrow v_1 = v_2 $$$

Lean4

@[ext]
theorem ext {v₁ v₂ : Valuation R Γ₀} (h : ∀ r, v₁ r = v₂ r) : v₁ = v₂ :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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