R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑↑(expand R p) f)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalRingHom ↑(expand R p)
refine' ⟨fun f hf1 => _⟩
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑↑(expand R p) f)
⊢ IsUnit f
norm_cast at hf1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff (↑(expand R p) f) 0)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
⊢ IsUnit f
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff (↑(expand R p) f) 0)
⊢ IsUnit f
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
rw [hf2, isUnit_C] at hf1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : f = ↑C (coeff f 0)
⊢ IsUnit f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
rw [expand_eq_C hp] at hf2
no goals
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : f = ↑C (coeff f 0)
⊢ IsUnit f
rwa [hf2, isUnit_C]