mulSupport_mulSingle_of_ne — Mathlib

English

If a ≠ 1, then mulSingle i a has exactly support {i}.

Русский

Если a ≠ 1, то mulSingle i a имеет опору ровно {i}.

LaTeX

$$$ a \neq 1 \Rightarrow \operatorname{mulSupport}(\mathrm{Pi}.\mathrm{mulSingle} i a) = \{ i \} $$$

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_mulSingle_of_ne (h : a ≠ 1) : mulSupport (mulSingle i a) = { i } :=
  mulSupport_mulSingle_subset.antisymm fun x hx ↦ by rwa [mem_mulSupport, hx, mulSingle_eq_same]

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