toIocMod_toIcoMod — Mathlib

English

Theorem toIcoMod_inj states that toIcoMod hp c a = toIcoMod hp c b holds iff a ≡ b [PMOD p].

Русский

Теорема toIcoMod_inj утверждает, что toIcoMod hp c a = toIcoMod hp c b эквивалентно a ≡ b [PMOD p].

LaTeX

$$$ toIcoMod\\ hp\\ c\\ a = toIcoMod\\ hp\\ c\\ b \\iff a \\equiv b\\ [PMOD\\ p] $$$

Lean4

@[simp]
theorem toIocMod_toIcoMod (a₁ a₂ b : α) : toIocMod hp a₁ (toIcoMod hp a₂ b) = toIocMod hp a₁ b :=
  (toIocMod_eq_toIocMod _).2 ⟨toIcoDiv hp a₂ b, self_sub_toIcoMod hp a₂ b⟩

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