fract_fract

Mathlib.Algebra.Module.ZLattice.Basic

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

← MathLib Explorer

English

The value of fractRestrict b at x equals fract b x when viewed in E.

Русский

Значение fractRestrict b на x равно fract b x, когда мы рассматриваем его в E.

LaTeX

$$$ (\operatorname{fractRestrict}\,b)(x) = \operatorname{fract}_b(x) $$$

Lean4

@[simp]
theorem fract_fract (m : E) : fract b (fract b m) = fract b m :=
  Basis.ext_elem b fun _ => by classical simp only [repr_fract_apply, Int.fract_fract]

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

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

Разделы

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

Аффилиация

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