irrational_div_natCast_iff — Mathlib

English

For every natural n and real x, Irrational(x / n) iff n ≠ 0 and Irrational x.

Русский

Пусть n ∈ ℕ. Тогда Irrational(x / n) эквивалентно (n ≠ 0 ∧ Irrational x).

LaTeX

$$$\\forall n \\in \\mathbb{N}, x \\in \\mathbb{R}, \\operatorname{Irrational}(x / n) \\iff (n \\neq 0 \\land \\operatorname{Irrational}(x))$$$

Lean4

@[simp]
theorem irrational_div_natCast_iff : Irrational (x / n) ↔ n ≠ 0 ∧ Irrational x := by
  rw [← cast_natCast, irrational_div_ratCast_iff, Nat.cast_ne_zero]

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