cast_le — Mathlib

English

For all m,n ∈ ZNum, (m:α) ≤ n iff m ≤ n when α is a ring with linear order.

Русский

Для всех m,n ∈ ZNum, (m:α) ≤ n эквивалентно m ≤ n при α, линейном порядке.

LaTeX

$$$$\forall {m,n} \in ZNum,\ (m : \alpha) \le n \leftrightarrow m \le n.$$$$

Lean4

@[simp, norm_cast]
theorem cast_le [Ring α] [LinearOrder α] [IsStrictOrderedRing α] {m n : ZNum} : (m : α) ≤ n ↔ m ≤ n := by rw [← not_lt];
  exact not_congr cast_lt

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