R : Type u
S : Type v
T : Type w
inst✝¹ : NonAssocSemiring R
M : Submonoid R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
n : ℕ
⊢ n • 1 ∈ s
R : Type u
S : Type v
T : Type w
inst✝¹ : NonAssocSemiring R
M : Submonoid R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
n : ℕ
⊢ ↑n ∈ s
rw [← nsmul_one]
no goals
R : Type u
S : Type v
T : Type w
inst✝¹ : NonAssocSemiring R
M : Submonoid R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
n : ℕ
⊢ n • 1 ∈ s
exact nsmul_mem (one_mem _) _