closure_pow — Mathlib

English

A refined version of closure_pow using the HPow and nat induction principle.

Русский

Уточнённая версия closure_pow с использованием HPow и индукции по натуральным.

LaTeX

$$$ \text{closure}(s^n) = \text{closure}(s) \text{ for } n \ge 1 $$$

Lean4

@[to_additive]
theorem closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

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