repr_floor_apply — Mathlib

English

If m lies in the ℤ-span of the basis range, then floor b m equals m.

Русский

Если m ∈ spanℤ(range b), то floor b m = m.

LaTeX

$$$ m \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range}(b)) \Rightarrow \operatorname{floor}_b(m) = m $$$

Lean4

@[simp]
theorem repr_floor_apply (m : E) (i : ι) : b.repr (floor b m) i = ⌊b.repr m i⌋ := by
  classical
    simp only [floor, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply, Finset.sum_apply',
    Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum, Finset.mem_univ, if_true,
    coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Похожие утверждения