R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
⊢ IsInteger R 0
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
⊢ IsInteger R (a • 0)
rw [smul_zero]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
⊢ IsInteger R 0
exact isInteger_zero
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
x y : P
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • x + a • y)
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
x y : P
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • (x + y))
rw [smul_add]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s → IsInteger R (a • b)
b : P
hb : b ∈ span R s
x y : P
hx : IsInteger R (a • x)
hy : IsInteger R (a • y)
⊢ IsInteger R (a • x + a • y)
exact isInteger_add hx hy
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s✝ : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
b : P
hb : b ∈ span R s✝
s : R
x : P
hx : IsInteger R (a • x)
⊢ IsInteger R (s • a • x)
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s✝ : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
b : P
hb : b ∈ span R s✝
s : R
x : P
hx : IsInteger R (a • x)
⊢ IsInteger R (a • s • x)
rw [smul_comm]
no goals
R : Type u_2
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_1
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
P' : Type ?u.659673
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.660126
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
I J : FractionalIdeal S P
g : P →ₐ[R] P'
s✝ : Set P
x✝ : ∃ a, a ∈ S ∧ ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
a : R
a_mem : a ∈ S
h : ∀ (b : P), b ∈ s✝ → IsInteger R (a • b)
b : P
hb : b ∈ span R s✝
s : R
x : P
hx : IsInteger R (a • x)
⊢ IsInteger R (s • a • x)
exact isInteger_smul hx