Theorem Ordinal.log_opow_mul

Modification history

2024-10-10 23:04
Mathlib/SetTheory/Ordinal/Exponential.lean
feat(SetTheory/Ordinal/Exponential): `log b x = y ↔ x ∈ Set.Ico (b ^ y) (b ^ (succ y))` (#15930) …
Added Ordinal.log_opow_mulView on Github →