pow_eq_closure_pow_set

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.pow_eq_closure_pow_set

English

Same as above: s^n = closure((s : Set R)^n) for a AddSubmonoid s in a semiring.

Русский

То же самое: s^n = closure((s : Set R)^n) для AddSubmonoid s в полукольце.

LaTeX

$$$ s^n = \operatorname{closure}((s : Set R)^n) $$$

Lean4

theorem pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) : s ^ n = closure ((s : Set R) ^ n) := by
  rw [← closure_pow, closure_eq]

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

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

Разделы

Аффилиация

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