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 v : E
h : v ∈ span ℤ (Set.range ↑b)
⊢ fract b (v + m) = fract b m
classical
refine (Basis.ext_elem_iff b).mpr fun i => ?_
simp_rw [repr_fract_apply, Int.fract_eq_fract]
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
  ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (fract b (v + m))) i = ↑(↑b.repr (fract b m)) i
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
⊢ fract b (v + m) = fract b m
refine (Basis.ext_elem_iff b).mpr fun i => ?_
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ∃ z, ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑z
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (fract b (v + m))) i = ↑(↑b.repr (fract b m)) i
simp_rw [repr_fract_apply, Int.fract_eq_fract]
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑(↑(↑(Basis.restrictScalars ℤ b).repr { val := v, property := h }) i)
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ∃ z, ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑z
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
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 v : E
h : v ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑(↑b.repr (v + m)) i - ↑(↑b.repr m) i = ↑(↑(↑(Basis.restrictScalars ℤ b).repr { val := v, property := h }) i)
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
  ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]