no goals
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ ↑(↑b.repr (fract b (fract b m))) x✝ = ↑(↑b.repr (fract b m)) x✝
classical simp only [repr_fract_apply, Int.fract_fract]
no goals
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ ↑(↑b.repr (fract b (fract b m))) x✝ = ↑(↑b.repr (fract b m)) x✝
simp only [repr_fract_apply, Int.fract_fract]