mk_eq_one

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.ValueGroupWithZero.mk_eq_one

English

mk x y = 1 iff x ≤ᵥ y and y ≤ᵥ x.

Русский

mk x y = 1 эквивалентно x ≤ᵥ y и y ≤ᵥ x.

LaTeX

$$$ \operatorname{ValueGroupWithZero.mk} x y = 1 \iff x \le_v y \land y \le_v x$$$

Lean4

@[simp]
theorem mk_eq_one (x : R) (y : posSubmonoid R) : ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ y ∧ y ≤ᵥ x := by
  simp [← mk_one_one, mk_eq_mk]

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

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

Разделы

Аффилиация

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