no goals
E : Type u_3
ι : Type u_2
K : Type u_1
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr (fract b m)) i = Int.fract (↑(↑b.repr m) i)
rw [fract, LinearEquiv.map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]