Exponential

📁 Source: Mathlib/SetTheory/Ordinal/Exponential.lean

Statistics

Metric	Count
Definitions `instPow`	1
Theorems `add_log_le_log_mul`, `div_opow_log_lt`, `div_opow_log_pos`, `div_two_opow_log`, `iSup_pow`, `iSup_pow_natCast`, `isNormal_opow`, `isSuccLimit_opow`, `isSuccLimit_opow_left`, `le_log_of_opow_le`, `left_le_opow`, `left_lt_opow`, `log_eq_iff`, `log_eq_zero`, `log_le_self`, `log_mod_opow_log_lt_log_self`, `log_mono_right`, `log_of_left_le_one`, `log_one_left`, `log_one_right`, `log_opow`, `log_opow_mul`, `log_opow_mul_add`, `log_pos`, `log_zero_left`, `log_zero_right`, `lt_log_of_lt_opow`, `lt_omega0_omega0_opow`, `lt_omega0_opow`, `lt_omega0_opow_succ`, `lt_opow_iff_log_lt`, `lt_opow_iff_log_lt'`, `lt_opow_of_isSuccLimit`, `lt_opow_of_log_lt`, `lt_opow_succ_log_self`, `mod_opow_log_lt_self`, `natCast_opow`, `natCast_pow`, `omega0_opow_mul_nat_lt`, `one_lt_opow`, `one_lt_pow`, `one_opow`, `opow_add`, `opow_add_one`, `opow_dvd_opow`, `opow_dvd_opow_iff`, `opow_eq_zero`, `opow_le_iff_le_log`, `opow_le_iff_le_log'`, `opow_le_of_isSuccLimit`, `opow_le_of_le_log`, `opow_le_opow`, `opow_le_opow_iff_right`, `opow_le_opow_left`, `opow_le_opow_right`, `opow_limit`, `opow_log_le_self`, `opow_lt_opow_iff_right`, `opow_lt_opow_left_of_succ`, `opow_mul`, `opow_mul_add_lt_opow`, `opow_mul_add_lt_opow_mul`, `opow_mul_add_pos`, `opow_mul_lt_opow`, `opow_natCast`, `opow_ne_zero`, `opow_one`, `opow_one_add`, `opow_pos`, `opow_right_inj`, `opow_succ`, `opow_zero`, `right_le_opow`, `two_opow_log_add`, `zero_opow`, `zero_opow'`, `zero_opow_le`	77
Total	78

Ordinal

Definitions

Name	Category	Theorems
`instPow` 📖	CompOp	143 math math: `opow_mul`, `opow_le_opow_right`, `lt_omega0_opow_succ`, `iSup_pow_natCast`, `opow_one`, `isPrincipal_add_iff_zero_or_omega0_opow`, `invVeblen₂_eq_iff`, `le_invVeblen₂_iff`, `CNF.eval_single_add'`, `opow_omega0`, `div_two_opow_log`, `CNF.coeff_opow_mul_add`, `principal_opow_ord`, `epsilon_eq_deriv`, `isPrincipal_mul_omega0_opow_opow`, `opow_add`, `nfp_mul_opow_omega0_add`, `div_opow_log_pos`, `isSuccLimit_opow_left`, `left_lt_opow`, `opow_mul_add_pos`, `principal_opow_omega0`, `isSuccLimit_opow`, `invVeblen₂_le_iff`, `mul_lt_omega0_opow`, `card_omega0_opow`, `iSup_pow`, `zero_opow'`, `eq_zero_or_opow_omega0_le_of_mul_eq_right`, `opow_log_le_self`, `right_le_opow`, `log_opow_mul`, `natCast_opow`, `opow_one_add`, `opow_dvd_opow`, `opow_mul_add_lt_opow`, `opow_le_opow_iff_right`, `veblen_opow_eq_opow_iff`, `div_opow_log_lt`, `CNF.eval_single`, `lt_epsilon_zero`, `iterate_omega0_opow_lt_epsilon0`, `lt_opow_succ_log_self`, `log_opow`, `nfp_mul_eq_opow_omega0`, `ONote.repr_scale`, `isPrincipal_opow_omega0`, `IsInitial.principal_opow`, `veblen_zero`, `isNormal_opow`, `one_opow`, `isPrincipal_add_opow_of_isPrincipal_add`, `opow_limit`, `CNF.eval_lt`, `mul_eq_right_iff_opow_omega0_dvd`, `ONote.omega0_le_oadd`, `opow_mul_add_lt_opow_mul`, `principal_add_iff_zero_or_omega0_opow`, `zero_opow_le`, `isPrincipal_opow_ord`, `epsilon_succ_eq_nfp`, `card_opow_le_of_omega0_le_right`, `ONote.repr_opow_aux₁`, `log_opow_mul_add`, `card_opow_omega0`, `opow_dvd_opow_iff`, `mem_range_veblen_iff_le_invVeblen₁`, `ONote.split_add_lt`, `natCast_opow_omega0`, `mod_opow_log_lt_self`, `mul_eq_opow_log_succ`, `veblen_invVeblen₁_invVeblen₂`, `lt_omega0_opow`, `ONote.repr_opow`, `log_eq_iff`, `CNF.foldr`, `lt_opow_iff_log_lt'`, `log_mod_opow_log_lt_log_self`, `epsilon0_eq_nfp`, `epsilon_zero_eq_nfp`, `veblen_mem_range_opow`, `card_opow_eq_of_omega0_le_right`, `CNF.rec_pos`, `lt_opow_of_log_lt`, `deriv_mul_eq_opow_omega0_mul`, `opow_natCast`, `opow_le_opow`, `ONote.NF.of_dvd_omega0_opow`, `opow_zero`, `opow_lt_veblen_opow_iff`, `two_opow_log_add`, `card_opow_le_of_omega0_le_left`, `mul_le_right_iff_opow_omega0_dvd`, `Mathlib.Meta.NormNum.isNat_ordinalOPow`, `card_opow_eq_of_omega0_le_left`, `opow_add_one`, `principal_mul_omega0_opow_opow`, `principal_opow_omega`, `lt_opow_of_isSuccLimit`, `omega0_opow_mul_nat_lt`, `CNF.ne_zero`, `invVeblen₂_lt_iff`, `add_omega0_opow`, `CNF.opow_mul_add`, `isPrincipal_mul_iff_le_two_or_omega0_opow_opow`, `CNF.eval_single_add`, `opow_mul_lt_opow`, `IsInitial.isPrincipal_opow`, `NONote.repr_opow`, `opow_lt_opow_iff_right`, `ONote.repr_opow_aux₂`, `invVeblen₂_lt`, `lt_invVeblen₂_iff`, `mul_omega0_opow_opow`, `veblen_eq_opow_iff`, `one_lt_opow`, `principal_add_omega0_opow`, `nfp_mul_one`, `opow_succ`, `veblen_zero_apply`, `opow_le_iff_le_log`, `opow_lt_opow_left_of_succ`, `ONote.scale_opowAux`, `opow_right_inj`, `iterate_omega0_opow_lt_epsilon_zero`, `isPrincipal_add_omega0_opow`, `principal_add_opow_of_principal_add`, `zero_opow`, `card_opow_le`, `lt_omega0_omega0_opow`, `opow_pos`, `opow_le_of_le_log`, `isPrincipal_opow_omega`, `opow_le_iff_le_log'`, `opow_le_opow_left`, `opow_le_of_isSuccLimit`, `left_le_opow`, `ONote.NFBelow.repr_lt`, `principal_mul_iff_le_two_or_omega0_opow_opow`, `lt_epsilon0`, `omega0_opow_epsilon`, `lt_opow_iff_log_lt`, `opow_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_log_le_log_mul` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `add` `log` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`lt_or_ge` `opow_le_iff_le_log` `mul_ne_zero` `noZeroDivisors` `opow_add` `mul_le_mul'` `mulLeftMono` `mulRightMono` `opow_log_le_self` `log_of_left_le_one` `zero_add` `le_rfl`
`div_opow_log_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `div` `instPow` `log`	—	`lt_mul_iff_div_lt` `LT.lt.ne'` `opow_pos` `LT.lt.trans` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `opow_succ` `lt_opow_succ_log_self`
`div_opow_log_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `div` `instPow` `log`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `log_of_left_le_one` `opow_zero` `div_one` `pos_iff_ne_zero` `div_pos` `opow_ne_zero` `LT.lt.ne'` `opow_log_le_self`
`div_two_opow_log` 📖	mathematical	—	`Ordinal` `div` `instPow` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `log` `one`	—	`le_antisymm` `Nat.instAtLeastTwoHAddOfNat` `instNoMaxOrder` `div_opow_log_lt` `one_lt_two` `instZeroLEOneClass` `instNeZeroOne` `instAddLeftStrictMono` `canonicallyOrderedAdd` `div_opow_log_pos`
`iSup_pow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Monoid.toPow` `monoid` `instPow` `omega0`	—	`iSup_pow_natCast`
`iSup_pow_natCast` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Monoid.toPow` `monoid` `instPow` `omega0`	—	`LE.le.lt_or_eq` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne` `opow_natCast` `apply_omega0_of_isNormal` `isNormal_opow` `one_pow` `ciSup_const` `one_opow`
`isNormal_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Order.IsNormal` `Ordinal` `instLinearOrder` `instPow`	—	`LT.lt.trans` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `Order.IsNormal.of_succ_lt` `wellFoundedLT` `opow_succ` `mul_one` `mul_lt_mul_of_pos_left` `instPosMulStrictMono` `opow_pos` `opow_le_of_isSuccLimit` `LT.lt.ne'` `instReflLe`
`isSuccLimit_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Order.IsSuccLimit`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`Order.IsNormal.map_isSuccLimit` `isNormal_opow`
`isSuccLimit_opow_left` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`zero_or_succ_or_isSuccLimit` `opow_succ` `isSuccLimit_mul_right` `opow_pos` `Order.IsSuccLimit.bot_lt` `isSuccLimit_opow` `one_lt_of_isSuccLimit`
`le_log_of_opow_le` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Preorder.toLE` `instPow`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `log`	—	`eq_or_ne` `LT.lt.asymm` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `opow_eq_zero` `nonpos_iff_eq_zero` `canonicallyOrderedAdd` `opow_le_iff_le_log`
`left_le_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`opow_one` `le_or_gt` `lt_or_eq_of_le` `Order.lt_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `zero_opow` `one_ne_zero` `zero_le` `one_opow` `le_refl` `opow_le_opow_iff_right` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne`
`left_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`opow_one` `opow_lt_opow_iff_right`
`log_eq_iff` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`log` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `Preorder.toLT` `Order.succ` `instSuccOrder`	—	`opow_log_le_self` `lt_opow_succ_log_self` `le_antisymm` `Order.lt_succ_iff` `instNoMaxOrder` `lt_opow_iff_log_lt` `opow_le_iff_le_log`
`log_eq_zero` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`log` `Ordinal` `zero`	—	`eq_or_ne` `log_zero_right` `le_or_gt` `Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `log_zero_left` `log_one_left` `nonpos_iff_eq_zero` `Order.lt_add_one_iff` `zero_add` `lt_opow_iff_log_lt` `opow_one`
`log_le_self` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `log`	—	`eq_or_ne` `log_zero_right` `le_refl` `lt_or_ge` `LE.le.trans` `right_le_opow` `opow_log_le_self` `log_of_left_le_one` `canonicallyOrderedAdd`
`log_mod_opow_log_lt_log_self` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Preorder.toLE`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `log` `mod` `instPow`	—	`eq_or_ne` `log_zero_right` `log_pos` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `canonicallyOrderedAdd` `LE.le.trans` `LT.lt.le` `lt_opow_iff_log_lt` `mod_lt` `LT.lt.ne'` `opow_pos` `LT.lt.pos`
`log_mono_right` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `log`	—	`eq_or_ne` `log_zero_right` `canonicallyOrderedAdd` `lt_or_ge` `opow_le_iff_le_log` `LT.lt.ne'` `LT.lt.trans_le` `Ne.bot_lt` `LE.le.trans` `opow_log_le_self` `log_of_left_le_one` `le_refl`
`log_of_left_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `one`	`log` `Ordinal` `zero`	—	`Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `csSup_of_not_bddAbove` `not_bddAbove_Ici` `BddAbove.mono` `instZeroLEOneClass` `instNeZeroOne` `zero_opow` `csSup_empty` `one_opow` `Set.preimage_const` `instNoTopOrderOfNoMaxOrder` `bot_eq_zero'`
`log_one_left` 📖	mathematical	—	`log` `Ordinal` `one` `zero`	—	`log_of_left_le_one` `instReflLe`
`log_one_right` 📖	mathematical	—	`log` `Ordinal` `one` `zero`	—	`lt_or_ge` `log_eq_zero` `log_of_left_le_one`
`log_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`log` `Ordinal` `instPow`	—	`mul_one` `log_one_right` `add_zero` `log_opow_mul` `zero_ne_one` `instNeZeroOne`
`log_opow_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`log` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `add`	—	`add_zero` `log_opow_mul_add` `opow_pos` `bot_lt_of_lt`
`log_opow_mul_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `instPow`	`log` `Ordinal` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	—	`log_eq_iff` `mul_ne_zero` `noZeroDivisors` `opow_ne_zero` `LT.lt.ne'` `bot_lt_of_lt` `left_eq_zero_of_add_eq_zero` `opow_add` `le_imp_le_of_le_of_le` `mul_le_mul_right` `mulLeftMono` `opow_log_le_self` `le_refl` `le_self_add` `canonicallyOrderedAdd` `LT.lt.trans_le` `add_lt_add_right` `instAddLeftStrictMono` `mul_add_one` `leftDistribClass` `Order.succ_eq_add_one` `add_assoc` `Order.add_one_le_iff` `instNoMaxOrder` `lt_opow_succ_log_self`
`log_pos` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Preorder.toLE`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `log`	—	`Order.add_one_le_iff` `instNoMaxOrder` `zero_add` `opow_le_iff_le_log` `opow_one`
`log_zero_left` 📖	mathematical	—	`log` `Ordinal` `zero`	—	`log_of_left_le_one` `canonicallyOrderedAdd`
`log_zero_right` 📖	mathematical	—	`log` `Ordinal` `zero`	—	`eq_or_ne` `log_zero_left` `Set.ext` `canonicallyOrderedAdd` `csSup_empty`
`lt_log_of_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `log`	—	`lt_imp_lt_of_le_imp_le` `opow_le_of_le_log`
`lt_omega0_omega0_opow` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`lt_omega0_opow` `opow_ne_zero` `omega0_ne_zero` `LT.lt.trans` `opow_mul_lt_opow` `natCast_lt_omega0` `LT.lt.trans_le` `mul_le_mul_right` `mulLeftMono` `Nat.cast_le` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `Nat.cast_add` `Nat.cast_one` `instPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `instAddLeftStrictMono` `instAddLeftReflectLT` `instNoMaxOrder` `canonicallyOrderedAdd` `mul_one`
`lt_omega0_opow` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`lt_log_of_lt_opow` `lt_omega0` `div_opow_log_lt` `one_lt_omega0` `natCast_succ` `lt_mul_succ_div` `opow_ne_zero` `omega0_ne_zero` `LT.lt.trans` `omega0_opow_mul_nat_lt`
`lt_omega0_opow_succ` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `Order.succ` `instSuccOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`lt_omega0_opow` `add_one_ne_zero` `LT.lt.trans_le` `le_imp_le_of_le_of_le` `mul_le_mul_left` `mulRightMono` `opow_le_opow` `le_refl` `Order.lt_succ_iff` `instNoMaxOrder` `omega0_pos` `LT.lt.trans` `omega0_opow_mul_nat_lt` `Order.lt_succ`
`lt_opow_iff_log_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `log`	—	`lt_iff_lt_of_le_iff_le` `opow_le_iff_le_log`
`lt_opow_iff_log_lt'` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `log`	—	`lt_iff_lt_of_le_iff_le` `opow_le_iff_le_log'`
`lt_opow_of_isSuccLimit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`Iff.not` `opow_le_of_isSuccLimit`
`lt_opow_of_log_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `log`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`lt_imp_lt_of_le_imp_le` `le_log_of_opow_le`
`lt_opow_succ_log_self` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `Order.succ` `instSuccOrder` `log`	—	`eq_or_ne` `log_zero_right` `Order.succ_eq_add_one` `zero_add` `opow_one` `LT.lt.pos` `canonicallyOrderedAdd` `lt_opow_iff_log_lt` `Order.lt_succ_iff` `instNoMaxOrder` `le_refl`
`mod_opow_log_lt_self` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `mod` `instPow` `log`	—	`eq_or_ne` `log_of_left_le_one` `canonicallyOrderedAdd` `opow_zero` `mod_one` `pos_iff_ne_zero` `LT.lt.trans_le` `mod_lt` `opow_ne_zero` `opow_log_le_self`
`natCast_opow` 📖	mathematical	—	`Ordinal` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Monoid.toPow` `Nat.instMonoid` `instPow`	—	`natCast_pow` `opow_natCast`
`natCast_pow` 📖	mathematical	—	`Ordinal` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Monoid.toPow` `Nat.instMonoid` `monoid`	—	`pow_zero` `Nat.cast_one` `pow_succ` `natCast_mul`
`omega0_opow_mul_nat_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`lt_of_lt_of_le` `opow_succ` `mul_lt_mul_of_pos_left` `instPosMulStrictMono` `natCast_lt_omega0` `opow_pos` `omega0_pos` `opow_le_opow_right` `Order.succ_le_of_lt`
`one_lt_opow` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `instPow`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_or_eq` `Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `zero_opow_le` `one_opow` `instReflLe` `opow_zero` `opow_lt_opow_iff_right` `pos_iff_ne_zero`
`one_lt_pow` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Monoid.toPow` `monoid`	—	`Nat.cast_one` `Nat.cast_zero` `opow_natCast` `instCharZero` `one_lt_opow`
`one_opow` 📖	mathematical	—	`Ordinal` `instPow` `one`	—	`opow_zero` `opow_succ` `mul_one` `eq_of_forall_ge_iff` `opow_le_of_isSuccLimit` `one_ne_zero` `Order.IsSuccLimit.bot_lt`
`opow_add` 📖	mathematical	—	`Ordinal` `instPow` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `add_zero` `opow_zero` `mul_one` `LT.lt.ne'` `LT.lt.trans_le` `le_add_self` `zero_opow` `MulZeroClass.mul_zero` `LE.le.eq_or_lt` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `one_opow` `Order.succ_eq_add_one` `add_assoc` `opow_add_one` `mul_assoc` `eq_of_forall_ge_iff` `Order.IsNormal.le_iff_forall_le` `Order.IsNormal.comp` `isNormal_opow` `isNormal_add_right` `isNormal_mul_right` `opow_pos` `pos_iff_ne_zero`
`opow_add_one` 📖	mathematical	—	`Ordinal` `instPow` `add` `one` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_or_ne` `zero_opow` `add_one_ne_zero` `MulZeroClass.mul_zero` `limitRecOn_succ`
`opow_dvd_opow` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `monoidWithZero` `instPow`	—	`opow_add` `add_sub_cancel_of_le`
`opow_dvd_opow_iff` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `monoidWithZero` `instPow` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	—	`le_of_not_gt` `not_le_of_gt` `opow_lt_opow_iff_right` `le_of_dvd` `opow_ne_zero` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `canonicallyOrderedAdd` `LT.lt.le` `opow_dvd_opow`
`opow_eq_zero` 📖	mathematical	—	`Ordinal` `instPow` `zero`	—	`opow_zero` `instNeZeroOne` `zero_opow`
`opow_le_iff_le_log` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `log`	—	`Order.IsNormal.le_iff_le_sSup'` `wellFoundedLT` `isNormal_opow` `opow_zero` `instZeroLEOneClass` `instNeZeroOne` `canonicallyOrderedAdd`
`opow_le_iff_le_log'` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `log`	—	`eq_or_ne` `canonicallyOrderedAdd` `log_zero_right` `bot_eq_zero'` `LT.lt.ne_bot` `opow_le_iff_le_log`
`opow_le_of_isSuccLimit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`opow_limit` `iSup_le_iff` `small_Iio`
`opow_le_of_le_log` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `log`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`le_or_gt` `LE.le.not_gt` `log_of_left_le_one` `pos_iff_ne_zero` `canonicallyOrderedAdd` `opow_le_iff_le_log'`
`opow_le_opow` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT` `zero`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`LE.le.trans` `opow_le_opow_left` `opow_le_opow_right`
`opow_le_opow_iff_right` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`StrictMono.le_iff_le` `Order.IsNormal.strictMono` `isNormal_opow`
`opow_le_opow_left` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`opow_zero` `instReflLe` `zero_opow` `canonicallyOrderedAdd` `Order.succ_eq_add_one` `opow_add_one` `mul_le_mul'` `mulLeftMono` `mulRightMono` `opow_le_of_isSuccLimit` `LE.le.trans` `opow_le_opow_right` `LT.lt.trans_le` `pos_iff_ne_zero` `LT.lt.le`
`opow_le_opow_right` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `Preorder.toLE`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`LE.le.eq_or_lt'` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne` `one_opow` `instReflLe` `opow_le_opow_iff_right`
`opow_limit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `instPow` `iSup` `Set.Elem` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`limitRecOn_limit`
`opow_log_le_self` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `log`	—	`le_or_gt` `Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `log_of_left_le_one` `opow_zero` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `instReflLe` `opow_le_iff_le_log` `le_refl`
`opow_lt_opow_iff_right` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`StrictMono.lt_iff_lt` `Order.IsNormal.strictMono` `isNormal_opow`
`opow_lt_opow_left_of_succ` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `Order.succ` `instSuccOrder`	—	`opow_succ` `mul_lt_mul_of_le_of_lt_of_nonneg_of_pos` `instPosMulStrictMono` `MulRightMono.toMulPosMono` `mulRightMono` `opow_le_opow_left` `le_of_lt` `zero_le` `canonicallyOrderedAdd` `opow_pos` `LT.lt.bot_lt`
`opow_mul` 📖	mathematical	—	`Ordinal` `instPow` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `MulZeroClass.zero_mul` `opow_zero` `one_opow` `eq_or_ne` `LT.lt.ne'` `MulZeroClass.mul_zero` `zero_opow` `noZeroDivisors` `LE.le.eq_or_lt` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `mul_succ` `opow_add` `opow_succ` `eq_of_forall_ge_iff` `Order.IsNormal.le_iff_forall_le` `Order.IsNormal.comp` `isNormal_opow` `isNormal_mul_right` `opow_le_of_isSuccLimit` `opow_ne_zero`
`opow_mul_add_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	—	`LT.lt.trans_le` `opow_mul_add_lt_opow_mul` `opow_succ` `opow_le_opow_right` `LT.lt.pos` `canonicallyOrderedAdd` `Order.succ_le_of_lt`
`opow_mul_add_lt_opow_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	—	`lt_of_lt_of_le` `mul_add_one` `leftDistribClass` `add_lt_add_iff_left` `instAddLeftStrictMono` `instAddLeftReflectLT` `le_imp_le_of_le_of_le` `mul_le_mul_right` `mulLeftMono` `Order.add_one_le_of_lt` `le_refl`
`opow_mul_add_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	—	`LT.lt.trans_le` `opow_pos` `pos_iff_ne_zero` `canonicallyOrderedAdd` `LE.le.trans` `le_mul_left` `le_self_add`
`opow_mul_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	—	`add_zero` `opow_mul_add_lt_opow` `opow_pos` `LT.lt.pos` `canonicallyOrderedAdd`
`opow_natCast` 📖	mathematical	—	`Ordinal` `instPow` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Monoid.toPow` `monoid`	—	`Nat.cast_zero` `opow_zero` `pow_zero` `Nat.cast_succ` `Order.succ_eq_add_one` `opow_succ` `pow_succ`
`opow_ne_zero` 📖	—	—	—	—	`pos_iff_ne_zero` `canonicallyOrderedAdd` `opow_pos`
`opow_one` 📖	mathematical	—	`Ordinal` `instPow` `one`	—	`zero_add` `opow_zero` `one_mul` `opow_add_one`
`opow_one_add` 📖	mathematical	—	`Ordinal` `instPow` `add` `one` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`opow_add` `opow_one`
`opow_pos` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `instPow`	—	`opow_zero` `instZeroLEOneClass` `instNeZeroOne` `opow_succ` `mul_pos` `instPosMulStrictMono` `lt_opow_of_isSuccLimit` `pos_iff_ne_zero` `canonicallyOrderedAdd` `Order.IsSuccLimit.bot_lt`
`opow_right_inj` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `instPow`	—	`StrictMono.injective` `Order.IsNormal.strictMono` `isNormal_opow`
`opow_succ` 📖	mathematical	—	`Ordinal` `instPow` `Order.succ` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`opow_add_one`
`opow_zero` 📖	mathematical	—	`Ordinal` `instPow` `zero` `one`	—	`eq_or_ne` `zero_opow'` `sub_zero` `limitRecOn_zero`
`right_le_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow`	—	`StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `isNormal_opow`
`two_opow_log_add` 📖	mathematical	—	`Ordinal` `add` `instPow` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `log` `mod`	—	`Nat.instAtLeastTwoHAddOfNat` `div_two_opow_log` `mul_one` `div_add_mod`
`zero_opow` 📖	mathematical	—	`Ordinal` `instPow` `zero`	—	`zero_opow'` `sub_eq_zero_iff_le` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `canonicallyOrderedAdd`
`zero_opow'` 📖	mathematical	—	`Ordinal` `instPow` `zero` `sub` `one`	—	—
`zero_opow_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `zero` `one`	—	`zero_opow'` `sub_le_self`

---

← Back to Index