Theorem: DividedPowerAlgebra.Ideal.map_coe_toRingHom (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra A R
inst✝ : Algebra A S
f : R →ₐ[A] S
I : Ideal R
⊢ Ideal.map f I = Ideal.map f.toRingHom I
Tactic:
rfl
State after:
no goals