R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type ?u.3235887
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3236124
inst✝⁹ : CommRing P
Rₘ : Type ?u.3236130
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
y : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap S Sₘ) (↑(algebraMap R S) ↑y))
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type ?u.3235887
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3236124
inst✝⁹ : CommRing P
Rₘ : Type ?u.3236130
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
y : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap R Sₘ) ↑y)
rw [IsScalarTower.algebraMap_apply _ S]
no goals
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type ?u.3235887
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3236124
inst✝⁹ : CommRing P
Rₘ : Type ?u.3236130
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
y : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap S Sₘ) (↑(algebraMap R S) ↑y))
exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩