one_le_cast

Mathlib.Data.Rat.Cast.Order

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

English

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

Русский

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

LaTeX

$$1 ≤ p.cast \iff 1 \le p$$

Lean4

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

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

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

Разделы

Аффилиация

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