cast_lt — Mathlib

English

For any α with a ring and order, (m:α) < n iff m < n for m,n ∈ ZNum.

Русский

Для любого кольца с порядком, (m:α) < n тогда и только тогда, когда m < n, для m,n ∈ ZNum.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_lt [Ring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum} : (m : α) < n ↔ m < n := by
  rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]

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