num_mul_denom_add_denom_mul_num_ne_zero

English

If x+y ≠ 0 in RatFunc K, then the linear combination x.num·y.denom + x.denom·y.num is nonzero.

Русский

Если x+y ≠ 0 в RatFunc K, то линейная комбинация x.num·y.denom + x.denom·y.num ненулевая.

LaTeX

$$$(x + y) \\neq 0 \\Rightarrow x\\text{.num} \\cdot y\\text{.denom} + x\\text{.denom} \\cdot y\\text{.num} \\neq 0$$$

Lean4

theorem num_mul_denom_add_denom_mul_num_ne_zero {x y : RatFunc K} (hxy : x + y ≠ 0) :
    x.num * y.denom + x.denom * y.num ≠ 0 := by
  intro h_zero
  have h := num_denom_add x y
  rw [h_zero, zero_mul] at h
  exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h

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