fract_eq_fract — Mathlib

English

When specializing to a singleton index set, floor reduces to the usual integer floor on the base field.

Русский

При одномерном базисе floor сводится к обычному целочисленному floor на базовом поле.

LaTeX

$$$ (\operatorname{floor}(\operatorname{Basis.singleton}\, \iota\, K)\ k).val = \lfloor k \rfloor $$$

Lean4

theorem fract_eq_fract (m n : E) : fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range b) := by
  classical
  rw [eq_comm, Basis.ext_elem_iff b]
  simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem, sub_eq_neg_add, map_add, map_neg,
    Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]

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