R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type u_1
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.565642
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } =
    { val := ↑(map g I) * ↑(map g J), property := (_ : IsFractional S (↑(map g I) * ↑(map g J))) }
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type u_1
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.565642
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g (I * J) = map g I * map g J
simp only [mul_def]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_3
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type u_1
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.565642
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
⊢ map g { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } =
    { val := ↑(map g I) * ↑(map g J), property := (_ : IsFractional S (↑(map g I) * ↑(map g J))) }
exact coeToSubmodule_injective (Submodule.map_mul _ _ _)