For singular strong limit κ, κ^{cf κ} = 2^κ

Proved

SingularCardinals.pow_cof_eq_two_pow_of_singular_strongLimit

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticset-theory

Let $\kappa$ be a singular strong limit cardinal, with cofinality $\operatorname{cf}\kappa<\kappa$ . Then

\kappa^{\operatorname{cf}\kappa}=2^\kappa.

This identity links the two forms of SCH: at a singular strong limit cardinal, the second form's conclusion $\kappa^{\operatorname{cf}\kappa}=\kappa^+$ is exactly the first form's $2^\kappa=\kappa^+$ .

Preamble

import Mathlib
import Definitions.Def_JechStationary
import Definitions.Def_SingularCardinals_basic

universe u

open Cardinal

Formal statement

namespace SingularCardinals

theorem pow_cof_eq_two_pow_of_singular_strongLimit (κ : Cardinal.{u})
    (hsing : κ.IsSingular) (hlim : IsStrongLimit κ) :
    κ ^ κ.ord.cof = 2 ^ κ := by sorry

end SingularCardinals

Source

Wikipedia, "Singular cardinals hypothesis", revision oldid=1349753131, https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131, paragraph "Another form of the SCH": "Note that κ^cf(κ) = 2^κ for all singular strong limit cardinals κ."

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph