floor_eq_self_of_mem — Mathlib

English

If m is in the lattice, floor b m equals the coordinate-wise floor across the basis.

Русский

Если m принадлежит решетке, floor b m равен по координатам по базису.

LaTeX

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

Lean4

@[simp]
theorem floor_eq_self_of_mem (m : E) (h : m ∈ span ℤ (Set.range b)) : (floor b m : E) = m :=
  by
  apply b.ext_elem
  simp_rw [repr_floor_apply b]
  intro i
  obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i
  rw [← hz]
  exact congr_arg (Int.cast : ℤ → K) (Int.floor_intCast z)

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