denom_mul_dvd — Mathlib

English

For RatFunc x and y over a field K, the denominator of the product x·y divides the product of the denominators: denom(xy) ∣ denom(x)·denom(y).

Русский

Для рациональных функций x и y над полем K знаменатель произведения x·y делится на произведение знаменателей denom(x)·denom(y).

LaTeX

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

Lean4

theorem denom_mul_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.num, ?_⟩
  rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]

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