Cardinal exponents

Stream: mathlib4

[Violeta Hernández]

I've got two questions about the current API on cardinal exponents.
a) Does it still make sense to call all the theorems about it using power instead of pow? I believe in Lean 3, the ^ symbol was tied to some stronger typeclass we couldn't use, but this isn't an issue anymore in Lean 4.
b) What's up with docs#Cardinal.powerlt ? I'm not asking to get rid of it or anything, but I'm curious to what it's used for or what it was meant for.

[Eric Wieser]

Usually we reserve pow for Nat powers; see zpow, rpow, etc

[Violeta Hernández]

Alright, so the convention still exists

[Violeta Hernández]

I do think it's a bit weird we went with power instead of something like cpow

[Yury G. Kudryashov]

We use cpow for complex powers, but probably these 2 APIs won't clash.

[Violeta Hernández]

Ah, makes sense. Yeah, I can't think of any other letter of the alphabet to use.

[Violeta Hernández]

Still curious about point b

[Sven Manthe]

I'm not sure if that's your question, but there are some (not formalized) theorems using it. The first example that comes to my mind - from model theory - is that if powerlt 2 κ≤κ is regular uncountable (which follows e.g. from GCH or κ being inaccessible), then there are saturated models of cardinality κ for any countable language.

[Violeta Hernández]

Ah, nice!

[Nir Paz]

I think the powerlt concept pops up just enough in and around cardinal arithmetic to warant a definition, mostly as a convenience (happy to be corrected though). Like in the above example it's equivalent to being inaccessible or a successor where GCH holds at the predecessor.

[Violeta Hernández]

Oh yeah, I'm not saying we get rid of it, especially now that I know there are important results involving it