Action

Statistics

Metric	Count
Definitions	0
Theorems `le_pow_smul`, `pow_smul_le`, `smul_iInf_le`, `smul_inf_le`, `smul_le_smul_left`, `smul_mono_right`, `smul_strictMono_right`	7
Total	7

Name	Kind	Assumes	Proves	Validates	Depends On
`le_pow_smul` 📖	mathematical	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`Monoid.toNatPow`	—	`pow_zero` `one_smul` `le_refl` `pow_succ'` `SemigroupAction.mul_smul` `LE.le.trans` `smul_mono_right`
`pow_smul_le` 📖	mathematical	`Preorder.toLE` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	`Monoid.toNatPow`	—	`pow_zero` `one_smul` `le_refl` `pow_succ'` `SemigroupAction.mul_smul` `LE.le.trans` `smul_mono_right`
`smul_iInf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_iInf` `smul_mono_right` `iInf_le`
`smul_inf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`Monotone.map_inf_le` `smul_mono_right`
`smul_le_smul_left` 📖	—	`Preorder.toLE`	—	—	`smul_mono_right`
`smul_mono_right` 📖	mathematical	—	`Monotone`	—	`CovariantClass.elim`
`smul_strictMono_right` 📖	mathematical	—	`StrictMono`	—	`CovariantClass.elim`

---