neg_divp

Mathlib.Algebra.Ring.Units

URI: https://scilib.ai/kg/mathlib#Units.neg_divp

English

Negating a division by a unit commutes with the division, i.e. -(a /ₚ u) = (-a) /ₚ u.

Русский

Отрицание деления на единицу коммутирует: - (a /ₚ u) = (-a) /ₚ u.

LaTeX

$$$-(a /_p u) = (-a) /_p u$$$

Lean4

theorem neg_divp (a : α) (u : αˣ) : -(a /ₚ u) = -a /ₚ u := by simp only [divp, neg_mul]

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

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

Разделы

Аффилиация

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