support_monomial — Mathlib

English

The support of a general monomial is either empty or a singleton depending on its coefficient.

Русский

Опора монома равна либо пустому множеству, либо единичному, в зависимости от коэффициента.

LaTeX

$$$[h: Decidable (a = 0)] : (monomial s a).support = if a = 0 then ∅ else { s }$$$

Lean4

theorem support_monomial [h : Decidable (a = 0)] : (monomial s a).support = if a = 0 then ∅ else { s } :=
  by
  rw [← Subsingleton.elim (Classical.decEq R a 0) h]
  rfl

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