noncommProd_singleton — Mathlib

English

The noncommutative product over a singleton {a} equals f(a).

Русский

Некоммопрод над единичным множеством {a} равен f(a).

LaTeX

$$$ noncommProd(\{a\}\; : \mathrm{Finset} \; \alpha) \; f \; comm = f(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem noncommProd_singleton (a : α) (f : α → β) :
    noncommProd ({ a } : Finset α) f
        (by
          norm_cast
          exact Set.pairwise_singleton _ _) =
      f a :=
  mul_one _

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