empty_zpow — Mathlib

English

The z-power of the empty Finset is empty for any nonzero integer exponent: (∅)^n = ∅ if n ≠ 0.

Русский

z-степень пустого Finset равна пустому набору при любом ненулевом целочисленном показателье.

LaTeX

$$s = ∅ ∧ n ≠ 0 ⇒ (∅ : Finset α)^n = ∅$$

Lean4

@[to_additive (attr := simp) zsmul_empty]
theorem empty_zpow (hn : n ≠ 0) : (∅ : Finset α) ^ n = ∅ := by cases n <;> simp_all

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