case intro
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
⊢ IsFractional S (span R ↑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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Submodule R P
hI : FG I
⊢ IsFractional S I
rcases hI with ⟨I, rfl⟩
case intro.intro.mk
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ (a : P), a ∈ I → IsInteger R (↑{ val := s, property := hs1 } • a)
⊢ IsFractional S (span R ↑I)
case intro
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
⊢ IsFractional S (span R ↑I)
rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩
case intro.intro.mk
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ (a : P), a ∈ I → IsInteger R (↑{ val := s, property := hs1 } • a)
⊢ ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ ↑I → IsInteger R (a • b)
case intro.intro.mk
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ (a : P), a ∈ I → IsInteger R (↑{ val := s, property := hs1 } • a)
⊢ IsFractional S (span R ↑I)
rw [isFractional_span_iff]
no goals
case intro.intro.mk
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
P' : Type ?u.669844
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.670297
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I✝ J : FractionalIdeal S P
g : P →ₐ[R] P'
I : Finset P
s : R
hs1 : s ∈ S
hs : ∀ (a : P), a ∈ I → IsInteger R (↑{ val := s, property := hs1 } • a)
⊢ ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ ↑I → IsInteger R (a • b)
exact ⟨s, hs1, hs⟩