Theorem Ordinal.log_opow_mul_add

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) …
Modified Ordinal.log_opow_mul_addView on Github →
2023-02-20 12:02
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: port SetTheory.Ordinal.Exponential (#2330)
Modified Ordinal.log_opow_mul_addView on Github →
2023-02-16 08:59
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: port SetTheory.Ordinal.Arithmetic (#2271)
Added Ordinal.log_opow_mul_addView on Github →