eq_one_iff_eq_one

Mathlib.RingTheory.Valuation.Basic

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

English

If v1 is equivalent to v2, then for all x, v1(x) = 1 iff v2(x) = 1.

Русский

Если v1 эквивалентна v2, то для каждого x верно: v1(x) = 1 ⇔ v2(x) = 1.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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