R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S 0
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S (0 • I)
rw [zero_smul]
case h.e'_7
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
x✝ : IsFractional S I
⊢ 0 = ↑↑0
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
x✝ : IsFractional S I
⊢ IsFractional S 0
convert((0 : Ideal R) : FractionalIdeal S P).isFractional
no goals
case h.e'_7
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
x✝ : IsFractional S I
⊢ 0 = ↑↑0
simp
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S (I + n • I)
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S ((n + 1) • I)
rw [succ_nsmul]
no goals
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I : Submodule R P
n : ℕ
h : IsFractional S I
⊢ IsFractional S (I + n • I)
exact h.sup (IsFractional.nsmul n h)