no goals
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ 0 < ↑(u * u)
exact this
no goals
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Module.Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v
rw [mul_smul, smul_inv_smul]