mul_left_cancel_iff'

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.mul_left_cancel_iff'

← MathLib Explorer

English

For c ≠ 0, c a ≡ c b mod (c m) iff a ≡ b mod m.

Русский

Для c ≠ 0 верно: c a ≡ c b mod (c m) тогда и только тогда, когда a ≡ b mod m.

LaTeX

$$$c \\neq 0 \\Rightarrow (c a \\equiv c b [ZMOD c m]) \\iff (a \\equiv b [ZMOD m]).$$$

Lean4

protected theorem mul_left_cancel_iff' (hc : c ≠ 0) : c * a ≡ c * b [ZMOD c * m] ↔ a ≡ b [ZMOD m] :=
  ⟨ModEq.mul_left_cancel' hc, Int.ModEq.mul_left'⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru