mul_cases — Mathlib

English

If the product x · y is irrational, then at least one of x or y is irrational.

Русский

Если произведение x · y иррационально, то хотя бы одно из x или y иррационально.

LaTeX

$$$$\operatorname{Irrational}(x y) \rightarrow \operatorname{Irrational}(x) \lor \operatorname{Irrational}(y).$$$$

Lean4

theorem mul_cases : Irrational (x * y) → Irrational x ∨ Irrational y :=
  by
  delta Irrational
  contrapose!
  rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩
  exact ⟨rx * ry, cast_mul rx ry⟩

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