neg_subst

Mathlib.Tactic.CancelDenoms.Core

URI: https://scilib.ai/kg/mathlib#CancelDenoms.neg_subst

Lean4

theorem neg_subst {α} [Ring α] {n e t : α} (h1 : n * e = t) : n * -e = -t := by simp [*]

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

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

Разделы

Аффилиация

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