denom_add_dvd — Mathlib

English

For x, y ∈ RatFunc(K) we have denom(x + y) ∣ denom(x) · denom(y).

Русский

Для любых x,y ∈ RatFunc(K) выполнено denom(x + y) ∣ denom(x) · denom(y).

LaTeX

$$$\\denom(x + y) \\mid \\denom(x) \\cdot \\denom(y)$$$

Lean4

theorem denom_add_dvd (x y : RatFunc K) : denom (x + y) ∣ denom x * denom y :=
  by
  rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]
  refine ⟨x.num * y.denom + x.denom * y.num, ?_⟩
  rw [RingHom.map_mul, RingHom.map_add, RingHom.map_mul, RingHom.map_mul, ← div_add_div, num_div_denom, num_div_denom]
  · exact algebraMap_ne_zero (denom_ne_zero x)
  · exact algebraMap_ne_zero (denom_ne_zero y)

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