fractRestrict_apply — Mathlib

English

Coordinate-wise equality of fract parts corresponds to a lattice difference, via an Exists witness.

Русский

Поштучное равенство дробных частей соответствует разности, лежащей в решетке, существует свидетель.

LaTeX

$$$ \exists z, m - n = z \;\text{ с } z \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range}(b)). $$$

Lean4

@[simp]
theorem fractRestrict_apply (x : E) : (fractRestrict b x : E) = fract b x :=
  rfl

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