n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map (RingHom.comp f (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S
rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
no goals
n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map (RingHom.comp f (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)
congr!