toIcoMod_inj — Mathlib

English

If the cycle modulo p is the same, then a ≡ b [PMOD p]. Equivalently, toIcoMod hp c a = toIcoMod hp c b iff a ≡ b [PMOD p].

Русский

Если значения по модулю p совпадают, то a эквивалентно b по модулю p. Аналогично, 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

/-- If `a` and `b` fall within the same cycle w.r.t. `c`, then they are congruent modulo `p`. -/
@[simp]
theorem toIcoMod_inj {c : α} : toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p] :=
  toIcoMod_eq_toIcoMod _

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