tfae_modEq — Mathlib

English

There is a chain of four equivalent statements: a ≡ b [PMOD p], (z) b − z p ∉ (a, a+p) for all integers z, toIcoMod hp a b ≠ toIocMod hp a b, and toIcoMod hp a b + p = toIocMod hp a b.

Русский

Существует цепочку из четырех эквивалентных утверждений: a ≡ b [PMOD p], ∀ z ∈ ℤ, b − z p ∉ (a, a+p), toIcoMod hp a b ≠ toIocMod hp a b, и toIcoMod hp a b + p = toIocMod hp a b.

LaTeX

$$$ \\text{TFAE}\\left[ a \\equiv b\\ [PMOD\\ p],\\ \\forall z:\\mathbb{Z},\\ b - z\\cdot p \\notin \\mathrm{Ioo}\\,a\\,(a+p),\\ toIcoMod\\ hp\\ a\\ b \\neq toIocMod\\ hp\\ a\\ b,\\ toIcoMod\\ hp\\ a\\ b + p = toIocMod\\ hp\\ a\\ b \\right] $$$

Lean4

theorem tfae_modEq :
    TFAE
      [a ≡ b [PMOD p], ∀ z : ℤ, b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
        toIcoMod hp a b + p = toIocMod hp a b] :=
  by
  rw [modEq_iff_toIcoMod_eq_left hp]
  tfae_have 3 → 2 := by
    rw [← not_exists, not_imp_not]
    exact fun ⟨i, hi⟩ =>
      ((toIcoMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ico_self hi, i, (sub_add_cancel b _).symm⟩).trans
        ((toIocMod_eq_iff hp).2 ⟨Set.Ioo_subset_Ioc_self hi, i, (sub_add_cancel b _).symm⟩).symm
  tfae_have 4 → 3
    | h => by
      rw [← h, Ne, eq_comm, add_eq_left]
      exact hp.ne'
  tfae_have 1 → 4
    | h => by
      rw [h, eq_comm, toIocMod_eq_iff, Set.right_mem_Ioc]
      refine ⟨lt_add_of_pos_right a hp, toIcoDiv hp a b - 1, ?_⟩
      rw [sub_one_zsmul, add_add_add_comm, add_neg_cancel, add_zero]
      conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, h]
  tfae_have 2 → 1 := by
    rw [← not_exists, not_imp_comm]
    have h' := toIcoMod_mem_Ico hp a b
    exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
  tfae_finish

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