cast_inv_le_one — Mathlib

English

In a semifield with a linear order and a strictly ordered ring structure, for every natural n, the inverse of n in α is at most 1.

Русский

Введите в полевую структуру с линейным порядком: для каждого натурального n обратное числа n в α не превосходит 1.

LaTeX

$$$ (n^{-1}) \le 1 \quad \text{for all } n \in \mathbb{N} $$$

Lean4

theorem cast_inv_le_one : ∀ n : ℕ, (n⁻¹ : α) ≤ 1
  | 0 => by simp
  | n + 1 => inv_le_one_of_one_le₀ <| by simp [Nat.cast_nonneg]

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