finset — Mathlib

English

If a is a unit in the monoid α, then the singleton Finset {a} is a unit in Finset α under pointwise multiplication.

Русский

Если a является единицей в моноиде α, то одиночное Finset {a} является единицей в Finset α с покооринованными по точечному умножению операциями.

LaTeX

$$IsUnit(a) \rightarrow IsUnit(\{a\} : Finset α)$$

Lean4

@[to_additive]
protected theorem _root_.IsUnit.finset : IsUnit a → IsUnit ({ a } : Finset α) :=
  IsUnit.map (singletonMonoidHom : α →* Finset α)

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