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
h : I ≤ 1
⊢ ∀ (b : P), b ∈ I → IsInteger R (1 • b)
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
h : I ≤ 1
⊢ IsFractional S I
use 1, S.one_mem
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
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)
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
h : I ≤ 1
⊢ ∀ (b : P), b ∈ I → IsInteger R (1 • b)
intro b hb
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
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b
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
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R (1 • b)
rw [one_smul]
case intro.refl
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
h : I ≤ 1
b' : R
hb : ↑(Algebra.linearMap R P) b' ∈ I
⊢ IsInteger R (↑(Algebra.linearMap R P) b')
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
h : I ≤ 1
b : P
hb : b ∈ I
⊢ IsInteger R b
obtain ⟨b', b'_mem, rfl⟩ := h hb
no goals
case intro.refl
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
h : I ≤ 1
b' : R
hb : ↑(Algebra.linearMap R P) b' ∈ I
⊢ IsInteger R (↑(Algebra.linearMap R P) b')
exact Set.mem_range_self b'