rel_refl

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

English

The valuative relation is reflexive: every element relates to itself.

Русский

Отношение валюативности рефлексивно: каждый элемент относится к самому себе.

LaTeX

$$$ x \leq\!_v x. $$$

Lean4

@[simp]
theorem rel_refl (x : R) : x ≤ᵥ x := by cases rel_total x x <;> assumption

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

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

Разделы

Аффилиация

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