le_one_iff_le_one

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.IsEquiv.le_one_iff_le_one

English

If v1 is equivalent to v2, then v1 x ≤ 1 iff v2 x ≤ 1 for all x in R.

Русский

Если v1 эквивалентна v2, то для всех x в R выполняется v1(x) ≤ 1 ⇔ v2(x) ≤ 1.

LaTeX

$$$ (v_1 \IsEquiv v_2) \rightarrow \forall x:\, R, v_1(x) \le 1 \iff v_2(x) \le 1 $$$

Lean4

theorem le_one_iff_le_one (h : v₁.IsEquiv v₂) {x : R} : v₁ x ≤ 1 ↔ v₂ x ≤ 1 := by rw [← v₁.map_one, h, map_one]

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

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

Разделы

Аффилиация

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