R : Type u
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : { x // x ∈ S }
⊢ Localization.mk a s • 1 = mk (↑(algebraMap R A) a) s
R : Type u
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : { x // x ∈ S }
⊢ ↑(algebraMap (Localization S) (LocalizedModule S ((fun x => A) a))) (Localization.mk a s) = mk (↑(algebraMap R A) a) s
rw [Algebra.algebraMap_eq_smul_one]
R : Type u
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : { x // x ∈ S }
⊢ Localization.mk a s • mk 1 1 = mk (↑(algebraMap R A) a) s
R : Type u
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : { x // x ∈ S }
⊢ Localization.mk a s • 1 = mk (↑(algebraMap R A) a) s
change _ • mk _ _ = _
no goals
R : Type u
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : { x // x ∈ S }
⊢ Localization.mk a s • mk 1 1 = mk (↑(algebraMap R A) a) s
rw [mk_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]