univ_pow — Mathlib

English

If α is a commutative monoid, then the set Set α with pointwise multiplication forms a commutative monoid.

Русский

Если α — коммутативный моноид, то множество Set α с поразличным поэлементному умножению образует коммутативный моноид.

LaTeX

$$$\text{If } \alpha \text{ is a commutative monoid, then } (Set\alpha) \text{ is a commutative monoid}$$$

Lean4

@[to_additive (attr := simp) nsmul_univ]
theorem univ_pow : ∀ {n : ℕ}, n ≠ 0 → (univ : Set α) ^ n = univ
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

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