zero_rel

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.zero_rel

English

0 is related to every x: 0 ≤ᵥ x for all x.

Русский

0 относится ко всем x: 0 ≤ᵥ x для всех x.

LaTeX

$$$ 0 \le\!_v x, \quad \forall x. $$$

Lean4

@[simp]
theorem zero_rel (x : R) : 0 ≤ᵥ x := by simpa using rel_mul_right x ((rel_total 0 1).resolve_right not_rel_one_zero)

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

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

Разделы

Аффилиация

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