case mp
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ denom x ∣ q → ∃ p, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q

case mpr
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) → denom x ∣ q
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ denom x ∣ q ↔ ∃ p, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
constructor
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
⊢ ∃ p_1, x = ↑(algebraMap K[X] (RatFunc K)) p_1 / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
case mp
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ denom x ∣ q → ∃ p, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q
rintro ⟨p, rfl⟩
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ ∃ p_1, x = ↑(algebraMap K[X] (RatFunc K)) p_1 / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
case mp.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
⊢ ∃ p_1, x = ↑(algebraMap K[X] (RatFunc K)) p_1 / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ x = ↑(algebraMap K[X] (RatFunc K)) (num x * p) / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ ∃ p_1, x = ↑(algebraMap K[X] (RatFunc K)) p_1 / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
use num x * p
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) p ≠ 0
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ x = ↑(algebraMap K[X] (RatFunc K)) (num x * p) / ↑(algebraMap K[X] (RatFunc K)) (denom x * p)
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom]
no goals
case mp.intro.intro
K : Type u
inst✝ : Field K
x : RatFunc K
p : K[X]
hq : denom x * p ≠ 0
_hx : denom x ≠ 0
hp : p ≠ 0
⊢ ↑(algebraMap K[X] (RatFunc K)) p ≠ 0
exact algebraMap_ne_zero hp
case mpr.intro
K : Type u
inst✝ : Field K
q : K[X]
hq : q ≠ 0
p : K[X]
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
case mpr
K : Type u
inst✝ : Field K
x : RatFunc K
q : K[X]
hq : q ≠ 0
⊢ (∃ p, x = ↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) → denom x ∣ q
rintro ⟨p, rfl⟩
no goals
case mpr.intro
K : Type u
inst✝ : Field K
q : K[X]
hq : q ≠ 0
p : K[X]
⊢ denom (↑(algebraMap K[X] (RatFunc K)) p / ↑(algebraMap K[X] (RatFunc K)) q) ∣ q
exact denom_div_dvd p q