| Name | Category | Theorems |
|---|
add 📖 | CompOp | 8 mathmath: canonicallyOrderedAdd, mk_add_mk, coe_add, instIsLeftCancelAddSubtypeLeOfNat, instIsRightCancelAddSubtypeLeOfNat, instIsCancelAddSubtypeLeOfNat, orderedSub, existsAddOfLE
|
addCancelCommMonoid 📖 | CompOp | — |
addCommMonoid 📖 | CompOp | 7 mathmath: segment_eq_uIcc, instArchimedean, isOrderedAddMonoid, NNReal.summable_mk, Icc_subset_segment, segment_eq_Icc, isOrderedCancelAddMonoid
|
addMonoid 📖 | CompOp | 1 mathmath: coeAddMonoidHom_apply
|
addMonoidWithOne 📖 | CompOp | — |
coeAddMonoidHom 📖 | CompOp | 1 mathmath: coeAddMonoidHom_apply
|
coeRingHom 📖 | CompOp | — |
commMonoidWithZero 📖 | CompOp | — |
commSemiring 📖 | CompOp | 4 mathmath: segment_eq_uIcc, Icc_subset_segment, instMulArchimedean, segment_eq_Icc
|
inhabited 📖 | CompOp | — |
monoidWithZero 📖 | CompOp | 6 mathmath: val_unitsEquivPos_symm_apply_coe, val_unitsHomeomorphPos_symm_apply_coe, val_inv_unitsHomeomorphPos_symm_apply_coe, unitsHomeomorphPos_apply_coe, unitsEquivPos_apply_coe, val_inv_unitsEquivPos_symm_apply_coe
|
mul 📖 | CompOp | 3 mathmath: mk_mul_mk, coe_mul, noZeroDivisors
|
natCast 📖 | CompOp | 2 mathmath: coe_natCast, mk_natCast
|
nsmul 📖 | CompOp | 3 mathmath: nsmul_mk, coe_nsmul, nsmul_coe
|
one 📖 | CompOp | 3 mathmath: mk_eq_one, NNReal.mk_one, coe_one
|
pow 📖 | CompOp | 2 mathmath: coe_pow, mk_pow
|
semiring 📖 | CompOp | 64 mathmath: ProperCone.dual_insert, ProperCone.dual_sUnion, isStrictOrderedRing, ProperCone.innerDual_univ, ProperCone.coe_positive, isOrderedRing, ProperCone.mem_map, PointedCone.coe_map, PointedCone.subset_dual_dual, ProperCone.coe_bot, segment_eq_uIcc, ProperCone.innerDual_sUnion, PointedCone.dual_union, ProperCone.innerDual_zero, PointedCone.mem_dual, PointedCone.dual_empty, instModuleFinite, ProperCone.dual_univ, PointedCone.dual_insert, ConvexCone.toPointedCone_top, PointedCone.convex, ProperCone.dual_iUnion, PointedCone.mem_map, PointedCone.coe_closure, ProperCone.innerDual_union, PointedCone.tmul_subset_maxTensorProduct, ProperCone.dual_zero, PointedCone.dual_zero, PointedCone.minTensorProduct_le_maxTensorProduct, PointedCone.tmul_subset_minTensorProduct, PointedCone.subset_span, PointedCone.ext_iff, ProperCone.innerDual_insert, PointedCone.dual_iUnion, PointedCone.mem_span_set, ProperCone.toPointedCone_bot, ProperCone.innerDual_empty, PointedCone.dual_le_dual, PointedCone.mem_closure, ProperCone.mem_bot, ProperCone.dual_empty, nat_ceil_coe, ProperCone.dual_union, PointedCone.mem_comap, Icc_subset_segment, PointedCone.mem_toConvexCone, nat_floor_coe, PointedCone.isClosed_dual, PointedCone.mem_positive, ProperCone.innerDual_iUnion, PointedCone.mem_maxTensorProduct, PointedCone.dual_flip_dual_dual_flip, ProperCone.mem_toPointedCone, PointedCone.dual_sUnion, ProperCone.innerDual_toSubmodule, ConvexCone.mem_toPointedCone, PointedCone.closure_eq, PointedCone.dual_univ, PointedCone.dual_eq_iInter_dual_singleton, PointedCone.dual_dual_flip_dual, PointedCone.coe_comap, segment_eq_Icc, PointedCone.salient_iff_inter_neg_eq_singleton, PointedCone.dual_span
|
sub 📖 | CompOp | 2 mathmath: mk_sub_mk, orderedSub
|
toNonneg 📖 | CompOp | 6 mathmath: toNonneg_of_nonneg, toNonneg_le, mk_sub_mk, coe_toNonneg, toNonneg_coe, toNonneg_lt
|
zero 📖 | CompOp | 7 mathmath: NNRat.mk_zero, coe_zero, mk_eq_zero, NNReal.mk_zero, instIsOrderedModule, noZeroDivisors, instIsStrictOrderedModule
|