case intro
R : Type u_1
R₂ : Type ?u.149702
K : Type ?u.149705
M : Type u_2
M₂ : Type ?u.149711
V : Type ?u.149714
S : Type ?u.149717
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
r : Rˣ
⊢ span R {↑r • x} = span R {x}
R : Type u_1
R₂ : Type ?u.149702
K : Type ?u.149705
M : Type u_2
M₂ : Type ?u.149711
V : Type ?u.149714
S : Type ?u.149717
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
r : R
hr : IsUnit r
x : M
⊢ span R {r • x} = span R {x}
lift r to Rˣ using hr
case intro
R : Type u_1
R₂ : Type ?u.149702
K : Type ?u.149705
M : Type u_2
M₂ : Type ?u.149711
V : Type ?u.149714
S : Type ?u.149717
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
r : Rˣ
⊢ span R {r • x} = span R {x}
case intro
R : Type u_1
R₂ : Type ?u.149702
K : Type ?u.149705
M : Type u_2
M₂ : Type ?u.149711
V : Type ?u.149714
S : Type ?u.149717
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
r : Rˣ
⊢ span R {↑r • x} = span R {x}
rw [← Units.smul_def]
no goals
case intro
R : Type u_1
R₂ : Type ?u.149702
K : Type ?u.149705
M : Type u_2
M₂ : Type ?u.149711
V : Type ?u.149714
S : Type ?u.149717
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
r : Rˣ
⊢ span R {r • x} = span R {x}
exact span_singleton_group_smul_eq R r x