emod_abs

Mathlib.Algebra.Order.Group.Unbundled.Int

URI: https://scilib.ai/kg/mathlib#Int.emod_abs

English

For all integers a,b, a mod |b| = a mod b.

Русский

Пусть a,b — целые числа. Тогда a mod |b| = a mod b.

LaTeX

$$$ a \bmod |b| = a \bmod b $$$

Lean4

@[simp]
theorem emod_abs (a b : ℤ) : a % |b| = a % b :=
  abs_by_cases (fun i => a % i = a % b) rfl (emod_neg _ _)

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

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

Разделы

Аффилиация

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