case pos
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

case neg
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J
by_cases H : J = 0
no goals
case pos
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J
rw [H, div_zero, map_zero, div_zero]
case neg
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ ↑(map ↑h { val := ↑I / ↑J, property := (_ : IsFractional R₁⁰ (↑I / ↑J)) }) =
    ↑{ val := ↑(map (↑h) I) / ↑(map (↑h) J), property := (_ : IsFractional R₁⁰ (↑(map (↑h) I) / ↑(map (↑h) J))) }
case neg
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J
rw [← coeToSubmodule_inj, div_nonzero H, div_nonzero (map_ne_zero _ H)]
no goals
case neg
R : Type ?u.1232681
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1232888
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J✝ : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ ↑(map ↑h { val := ↑I / ↑J, property := (_ : IsFractional R₁⁰ (↑I / ↑J)) }) =
    ↑{ val := ↑(map (↑h) I) / ↑(map (↑h) J), property := (_ : IsFractional R₁⁰ (↑(map (↑h) I) / ↑(map (↑h) J))) }
simp [Submodule.map_div]