zero_srel_one

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

English

0 is strictly smaller than 1 in the valuative relation: 0 <ᵥ 1.

Русский

0 строго меньше 1 по отношению валюативности: 0 <ᵥ 1.

LaTeX

$$$ 0 <\!_v 1. $$$

Lean4

@[simp]
theorem zero_srel_one : (0 : R) <ᵥ 1 :=
  not_rel_one_zero

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

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

Разделы

Аффилиация

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