R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
⊢ IsUnit f
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
⊢ IsUnit f
have dz := degree_eq_zero_of_isUnit H
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit f

case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
⊢ ↑φ (leadingCoeff f) ≠ 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
⊢ IsUnit f
rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit (↑C (coeff f 0))
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit f
rw [eq_C_of_degree_eq_zero dz]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit (coeff f 0)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit (↑C (coeff f 0))
refine' IsUnit.map C _
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = leadingCoeff f
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ IsUnit (coeff f 0)
convert hf
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = coeff f (natDegree f)
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = leadingCoeff f
change coeff f 0 = coeff f (natDegree f)
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = coeff f Zero.zero

R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ f ≠ 0
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = coeff f (natDegree f)
rw [(degree_eq_iff_natDegree_eq _).1 dz]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ f ≠ 0
case h.e'_3
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ coeff f 0 = coeff f Zero.zero

R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ f ≠ 0
rfl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hf : IsUnit (leadingCoeff 0)
H : IsUnit (map φ 0)
dz : degree 0 = 0
⊢ False
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree f = 0
⊢ f ≠ 0
rintro rfl
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hf : IsUnit (leadingCoeff 0)
H : IsUnit (map φ 0)
dz : degree 0 = 0
⊢ False
simp at H
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
⊢ False
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
⊢ ↑φ (leadingCoeff f) ≠ 0
intro h
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
u : IsUnit (↑φ (leadingCoeff f))
⊢ False
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
⊢ False
have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
u : IsUnit 0
⊢ False
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
u : IsUnit (↑φ (leadingCoeff f))
⊢ False
rw [h] at u
no goals
case hf
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit (leadingCoeff f)
H : IsUnit (map φ f)
dz : degree (map φ f) = 0
h : ↑φ (leadingCoeff f) = 0
u : IsUnit 0
⊢ False
simp at u