Deriv

📁 Source: Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean

Statistics

Metric	Count
Definitions	0
Theorems strictConvexOn_pow, prod_nonneg_of_card_nonpos_even, deriv2_sqrt_mul_log, deriv_sqrt_mul_log, deriv_sqrt_mul_log', hasDerivAt_sqrt_mul_log, int_prod_range_nonneg, int_prod_range_pos, strictConcaveOn_cos_Icc, strictConcaveOn_sin_Icc, strictConcaveOn_sqrt_mul_log_Ioi, strictConvexOn_pow, strictConvexOn_zpow	13
Total	13

Even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictConvexOn_pow 📖	mathematical	Even	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.univ Monoid.toPow Real.instMonoid	—	StrictMono.strictConvexOn_univ_of_deriv continuous_pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_pow_field StrictMono.const_mul IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Odd.strictMono_pow AddGroup.existsAddOfLE Nat.Even.sub_odd Nat.odd_iff Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_nonneg_of_card_nonpos_even 📖	mathematical	Even card filter Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing prod CommRing.toCommMonoid	—	prod_nonneg IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing neg_mul one_mul IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt lt_of_not_ge prod_mul_distrib prod_ite prod_const_one mul_one prod_const neg_one_pow_eq_pow_mod_two Nat.even_iff pow_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv2_sqrt_mul_log 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat deriv_sqrt_mul_log' le_or_gt Real.sqrt_eq_zero_of_nonpos zero_pow three_ne_zero MulZeroClass.mul_zero div_zero HasDerivWithinAt.deriv_eq_zero HasDerivWithinAt.congr_of_mem hasDerivWithinAt_const uniqueDiffOn_Iic Real.sqrt_ne_zero' Real.mul_self_sqrt LT.lt.le Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_pf_right HasDerivAt.deriv HasDerivAt.div HasDerivAt.const_add Real.hasDerivAt_log LT.lt.ne' HasDerivAt.const_mul Real.hasDerivAt_sqrt mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two
deriv_sqrt_mul_log 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat lt_or_ge HasDerivAt.deriv hasDerivAt_sqrt_mul_log LT.lt.ne' Real.sqrt_eq_zero_of_nonpos MulZeroClass.mul_zero div_zero HasDerivWithinAt.deriv_eq_zero HasDerivWithinAt.congr_of_mem hasDerivWithinAt_const MulZeroClass.zero_mul uniqueDiffOn_Iic
deriv_sqrt_mul_log' 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat deriv_sqrt_mul_log
hasDerivAt_sqrt_mul_log 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.sqrt Real.log DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Nat.instAtLeastTwoHAddOfNat IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul add_div div_mul_cancel_left₀ two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike div_eq_mul_inv Real.sqrt_div_self' add_comm one_div div_eq_inv_mul HasDerivAt.mul Real.hasDerivAt_sqrt Real.hasDerivAt_log
int_prod_range_nonneg 📖	mathematical	Even	Finset.prod Int.instCommMonoid Finset.range	—	Finset.prod_congr add_zero Int.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat two_mul mul_add Distrib.leftDistribClass mul_one one_add_one_eq_two add_assoc Finset.prod_range_succ mul_assoc mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing le_or_gt LE.le.trans LT.lt.le lt_add_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instAddLeftMono mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le sub_nonpos_of_le sub_nonneg_of_le
int_prod_range_pos 📖	mathematical	Even Set Set.instMembership Set.Ico PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder	Finset.prod Int.instCommMonoid Finset.range	—	LE.le.lt_of_ne int_prod_range_nonneg Finset.prod_eq_zero_iff Int.instNontrivial NormMulClass.toNoZeroDivisors Int.instNormMulClass sub_eq_zero Finset.mem_range
strictConcaveOn_cos_Icc 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc Real.instPreorder Real.instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos	—	strictConcaveOn_of_deriv2_neg Nat.instAtLeastTwoHAddOfNat convex_Icc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Real.continuousOn_cos Function.iterate_one Real.deriv_cos' deriv.fun_neg' Real.deriv_sin IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.cos_pos_of_mem_Ioo interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
strictConcaveOn_sin_Icc 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Icc Real.instPreorder Real.instZero Real.pi Real.sin	—	strictConcaveOn_of_deriv2_neg convex_Icc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Real.continuousOn_sin Function.iterate_one Real.deriv_sin Real.deriv_cos' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.sin_pos_of_mem_Ioo interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial
strictConcaveOn_sqrt_mul_log_Ioi 📖	mathematical	—	StrictConcaveOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instOne Real.instMul Real.sqrt Real.log	—	strictConcaveOn_of_deriv2_neg' convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.continuousOn Real.continuous_sqrt ContinuousOn.mono Real.continuousOn_log ne_of_gt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat deriv2_sqrt_mul_log div_neg_of_neg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono neg_neg_of_pos Real.instIsOrderedAddMonoid Real.log_pos mul_pos four_pos IsOrderedAddMonoid.toAddLeftMono pow_pos Real.sqrt_pos
strictConvexOn_pow 📖	mathematical	—	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero Monoid.toPow Real.instMonoid	—	StrictMonoOn.strictConvexOn_of_deriv convex_Ici Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing continuousOn_pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_pow_field interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial mul_lt_mul_of_pos_left pow_lt_pow_left₀ IsOrderedRing.toMulPosMono LT.lt.le Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat
strictConvexOn_zpow 📖	mathematical	—	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero DivInvMonoid.toZPow Real.instDivInvMonoid	—	strictConvexOn_of_deriv2_pos' convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing ContinuousOn.mono continuousOn_zpow₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ne_of_gt iter_deriv_zpow mul_pos IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero Finset.prod_congr Int.cast_natCast Int.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike int_prod_range_pos Int.instCharZero Nat.instAtLeastTwoHAddOfNat Finset.coe_Ico CharP.cast_eq_zero CharP.ofCharZero add_zero Nat.cast_one zero_add zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Set.mem_Ioi

---

← Back to Index