one_mem_pow — Mathlib

English

If 1 belongs to a subset s of a monoid, then 1 belongs to every n-th power s^n for all natural n.

Русский

Если 1 принадлежит подмножеству s моноида, то 1 принадлежит каждому элементу s^n при любом натуральном n.

LaTeX

$$$(1\in s) \Rightarrow (\forall n \in \mathbb{N}, 1 \in s^n)$$$

Lean4

@[to_additive]
theorem one_mem_pow (hs : 1 ∈ s) : 1 ∈ s ^ n := by simpa using pow_mem_pow hs

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