instBtwQuotientAddSubgroupZmultiples

English

The IcoMod value for (a, b) is the IcoMod value for (0, b−a) shifted by a.

Русский

Значение IcoMod для (a, b) равно значению IcoMod для (0, b−a), сдвинутому на a.

LaTeX

$$$$ \operatorname{toIcoMod}(hp, a, b) = \operatorname{toIcoMod}(hp, 0, b-a) + a $$$$

Lean4

instance : Btw (α ⧸ AddSubgroup.zmultiples p) where
  btw x₁ x₂ x₃ := (equivIcoMod hp'.out 0 (x₂ - x₁) : α) ≤ equivIocMod hp'.out 0 (x₃ - x₁)

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