R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ ↑f r * ↑f s ∈ map f I * map f J
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ ↑f (r * s) ∈ map f I * map f J
rw [_root_.map_mul]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ ↑f r * ↑f s ∈ map f I * map f J
exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj)
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
i : S
x✝¹ : i ∈ ↑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : ↑f r = i
j : S
x✝ : j ∈ ↑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : ↑f s = j
⊢ ↑f (r * s) ∈ ↑(map f (I * J))
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
i : S
x✝¹ : i ∈ ↑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : ↑f r = i
j : S
x✝ : j ∈ ↑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : ↑f s = j
⊢ ↑f r * ↑f s ∈ ↑(map f (I * J))
rw [← _root_.map_mul]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
i : S
x✝¹ : i ∈ ↑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : ↑f r = i
j : S
x✝ : j ∈ ↑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : ↑f s = j
⊢ ↑f (r * s) ∈ ↑(map f (I * J))
exact mem_map_of_mem f (mul_mem_mul hri hsj)