pow_mem_pow

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.pow_mem_pow

English

If a ∈ s, then a^n ∈ s^n.

Русский

Если a ∈ s, то a^n ∈ s^n.

LaTeX

$$$a \\in s \\Rightarrow a^n \\in s^n$$$

Lean4

@[to_additive]
theorem pow_mem_pow (ha : a ∈ s) : a ^ n ∈ s ^ n := by simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru