Overlap

Mathlib.Tactic.Ring.Basic

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Ring.Overlap

Lean4

/-- Two monomials are said to "overlap" if they differ by a constant factor, in which case the
constants just add. When this happens, the constant may be either zero (if the monomials cancel)
or nonzero (if they add up); the zero case is handled specially.
-/
inductive Overlap (e : Q($α)) where/-- The expression `e` (the sum of monomials) is equal to `0`. -/

  | zero (_ : Q(IsNat $e (nat_lit 0)))/-- The expression `e` (the sum of monomials) is equal to another monomial
  (with nonzero leading coefficient). -/

  | nonzero (_ : Result (ExProd sα) e)

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

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

Разделы

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

Аффилиация

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