fract_add_ZSpan — Mathlib

English

For any v in span ℤ(range b), fract b (v + m) = fract b m.

Русский

Для любого v из spanℤ(range b) выполняется fract b (v + m) = fract b m.

LaTeX

$$$ \operatorname{fract}_b(v + m) = \operatorname{fract}_b(m), \ v \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range}(b)) $$$

Lean4

@[simp]
theorem fract_add_ZSpan (m : E) {v : E} (h : v ∈ span ℤ (Set.range b)) : fract b (m + v) = fract b m := by
  rw [add_comm, fract_zSpan_add b m h]

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