R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
nontriviality S
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
haveI : Nontrivial R := f.domain_nontrivial
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this✝ : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
  div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
    ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq],
      calc
        _ ≤ degree (p %ₘ q) := degree_map_le _ _
        _ < degree q := (degree_modByMonic_lt _ hq)
        _ = _ :=
          Eq.symm <|
            degree_map_eq_of_leadingCoeff_ne_zero _
              (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this✝ : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q
exact ⟨this.1.symm, this.2.symm⟩
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)
rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div _ hq]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ ↑f (leadingCoeff q) ≠ 0
rw [Monic.def.1 hq, f.map_one]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hq : Monic q
✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
exact one_ne_zero