Commit 2024-10-10 23:04 c4139755
View on Github →feat(SetTheory/Ordinal/Exponential): log b x = y ↔ x ∈ Set.Ico (b ^ y) (b ^ (succ y)) (#15930)
We give a nice characterization for log b x = y. We then use it to prove a more general version of log_opow_mul_add, alongside other lemmas.