Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.mul_eq_opow_log_succ

Modification history

2022-07-22 09:11
src/set_theory/ordinal/principal.lean
chore(set_theory/ordinal/arithmetic): change `0 < x` assumptions to `x ≠ 0` (#15562) …
Modified ordinal.mul_eq_opow_log_succView on Github →
2022-03-29 07:35
src/set_theory/principal.lean
feat(set_theory/ordinal_arithmetic): Characterize principal multiplicative ordinals (#11701) …
Added ordinal.mul_eq_opow_log_succView on Github →