repr_fract_apply

Mathlib.Algebra.Module.ZLattice.Basic

URI: https://scilib.ai/kg/mathlib#ZSpan.repr_fract_apply

← MathLib Explorer

English

The map fractRestrict b: E → fundamentalDomain b is surjective.

Русский

Граф fractRestrict b: E → fundamentalDomain b сюръективно отображает пространство.

LaTeX

$$$ \text{Surjective}(\operatorname{fractRestrict}\,b) $$$

Lean4

@[simp]
theorem repr_fract_apply (m : E) (i : ι) : b.repr (fract b m) i = Int.fract (b.repr m i) := by
  rw [fract, map_sub, Finsupp.coe_sub, Pi.sub_apply, repr_floor_apply, Int.fract]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru