mulSupport_mulSingle — Mathlib

English

The mulSupport of mulSingle i a is either empty or {i} depending on whether a=1.

Русский

Опора mulSingle i a либо пуста, либо равна {i}, в зависимости от того, равна ли a 1.

LaTeX

$$$ \operatorname{mulSupport}(\mathrm{Pi}.\mathrm{mulSingle} i a) = \begin{cases} \emptyset, & a=1 \\ \{ i \}, & a \neq 1 \end{cases} $$$

Lean4

@[to_additive]
theorem mulSupport_mulSingle [DecidableEq M] : mulSupport (mulSingle i a) = if a = 1 then ∅ else { i } := by
  split_ifs with h <;> simp [h]

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