R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
⊢ p %ₘ 0 = p
haveI := monic_zero_iff_subsingleton.mp h
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p
simp
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0) * 0) < degree p);
          let dm := divModByMonicAux (p - z * 0) (_ : Monic 0);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ p %ₘ 0 = p
unfold modByMonic divModByMonicAux
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
h : ¬Monic 0
⊢ (if h : Monic 0 then
      (if h_1 : degree 0 ≤ degree p ∧ p ≠ 0 then
          let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0);
          let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree 0) * 0) < degree p);
          let dm := divModByMonicAux (p - z * 0) (_ : Monic 0);
          (z + dm.fst, dm.snd)
        else (0, p)).snd
    else p) =
    p
rw [dif_neg h]