repr_ceil_apply — Mathlib

English

The i-th coordinate of fract b m equals the fractional part (Int.fract) of the i-th coordinate of m.

Русский

i-я координата fract b m равна дробной частью (Int.fract) i-й координаты m.

LaTeX

$$$ b.repr(\operatorname{fract}_b(m))_i = \operatorname{Int.fract}(b.repr(m)_i) $$$

Lean4

@[simp]
theorem repr_ceil_apply (m : E) (i : ι) : b.repr (ceil b m) i = ⌈b.repr m i⌉ := by
  classical
    simp only [ceil, ← 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]

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