map_op_pow — Mathlib

English

For any Finset s, the map toEmbedding induced by opEquiv commutes with n-th powers: map_op_pow(s, n) = map_op_pow(s)^n.

Русский

Для любого Finset s отображение через opEquiv.toEmbedding коммутирует с n-разовыми степенями.

LaTeX

$$$(\mathrm{map}\, \mathrm{opEquiv.toEmbedding})(s^n) = (\mathrm{map}\, \mathrm{opEquiv.toEmbedding})(s)^n$$

Lean4

@[to_additive]
theorem map_op_pow (s : Finset α) : ∀ n : ℕ, (s ^ n).map opEquiv.toEmbedding = s.map opEquiv.toEmbedding ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => by rw [pow_succ, pow_succ', map_op_mul, map_op_pow]

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