K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x * y = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ denom (x * y) ∣ denom x * denom y
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x * y = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
refine' ⟨x.num * y.num, _⟩
no goals
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = ↑(algebraMap K[X] (RatFunc K)) (num x * num y) / ↑(algebraMap K[X] (RatFunc K)) (denom x * denom y)
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]