Theorem Ordinal.log_eq_iff

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_eq_iff View on Github →