cast_le_one

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#NNRat.cast_le_one

English

For p ∈ ℚ≥0, p.cast ≤ 1 if and only if p ≤ 1.

Русский

Для p ∈ ℚ≥0 верно: p.cast ≤ 1 ⇔ p ≤ 1.

LaTeX

$$$(p : K) \le 1 \iff p \le 1$$$

Lean4

@[simp]
theorem cast_le_one : (p : K) ≤ 1 ↔ p ≤ 1 := by norm_cast

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

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

Разделы

Аффилиация

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