coe_set_pow — Mathlib

English

Raising a submonoid to a positive power in a pointwise sense yields the same underlying set as the original submonoid, via the coercion to sets.

Русский

При возведении подмoноида в положительную степень по точечной инструкции получается та же самая подмножество как множество.

LaTeX

$$$ (H^n : Set M) = H \quad \text{for } n \neq 0 $$$

Lean4

@[to_additive (attr := simp)]
theorem coe_set_pow [SetLike S M] [SubmonoidClass S M] : ∀ {n} (_ : n ≠ 0) (H : S), (H ^ n : Set M) = H
  | 1, _, H => by simp
  | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

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