modEq_iff_toIcoDiv_eq_toIocDiv_add_one

English

A ≡ B [PMOD p] iff toIcoDiv hp a b = toIocDiv hp a b + 1.

Русский

A ≡ B [PMOD p] эквивалентно toIcoDiv hp a b = toIocDiv hp a b + 1.

LaTeX

$$$ a \\equiv b\\ [PMOD\\ p] \\iff toIcoDiv hp a b = toIocDiv hp a b + 1 $$$

Lean4

theorem modEq_iff_toIcoDiv_eq_toIocDiv_add_one : a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1 := by
  rw [modEq_iff_toIcoMod_add_period_eq_toIocMod hp, toIcoMod, toIocMod, ← eq_sub_iff_add_eq, sub_sub, sub_right_inj, ←
    add_one_zsmul, zsmul_left_inj hp]

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