coe_floor_self

Mathlib.Algebra.Module.ZLattice.Basic

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

← MathLib Explorer

English

The fract of any x lies in the fundamental domain of b.

Русский

Дробная часть fract b x принадлежит фундаментальной области b.

LaTeX

$$$ fract\_b(x) \in \operatorname{fundamentalDomain}(b) $$$

Lean4

@[simp]
theorem coe_floor_self (k : K) : (floor (Basis.singleton ι K) k : K) = ⌊k⌋ :=
  Basis.ext_elem (Basis.singleton ι K) fun _ => by rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]

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

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

Разделы

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

Аффилиация

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