order

📁 Source: MathlibTest/order.lean

Statistics

Metric	Count
Definitions order, order, order, order, order, order, order	7
Theorems order	1
Total	8

Configuration.ProjectivePlane

Definitions

Name	Category	Theorems
order 📖	CompOp	6 math math: card_points, lineCount_eq, one_lt_order, Dual.order, card_lines, pointCount_eq

Configuration.ProjectivePlane.Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
order 📖	mathematical	—	Configuration.ProjectivePlane.order Configuration.Dual Configuration.instMembershipDual Configuration.ProjectivePlane.instDual	—	Configuration.ProjectivePlane.exists_config Configuration.ProjectivePlane.lineCount_eq_pointCount Configuration.instFiniteDual

FirstOrder.Language

Definitions

Name	Category	Theorems
order 📖	CompOp	19 math math: orderLHom_leSymb, order.instSubsingleton, dlo_age, order.relation_eq_leSymb, orderLHom_order, instIsExpansionOnOrderLHomOfOrderedStructureOrder, isFraisse_finite_linear_order, order.card_eq_one, isFraisseLimit_of_countable_nonempty_dlo, dlo_isExtensionPair, order.instStrongHomClassOrderEmbedding, order.instIsEmptyRelationsOfNatNat, order.instHomClassOfOrderHomClass, order.instStrongHomClassOfOrderIsoClass, orderLHom_onRelation, dlo_isComplete, orderedStructure_iff, orderLHom_onFunction, aleph0_categorical_dlo

FormalMultilinearSeries

Definitions

Name	Category	Theorems
order 📖	CompOp	6 math math: order_eq_zero_iff, HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope, order_eq_zero_iff', order_eq_find', order_eq_find, order_zero

HahnSeries

Definitions

Name	Category	Theorems
order 📖	CompOp	32 math math: order_lt_iff_exists, order_neg, LaurentSeries.ofPowerSeries_powerSeriesPart, LaurentSeries.single_order_mul_powerSeriesPart, order_mul, order_single_mul_of_isRegular, order_abs, LaurentSeries.powerSeriesPart_coeff, order_mul_of_nonzero, HahnModule.coeff_smul_order_add_order, order_le_of_coeff_ne_zero, order_ofForallLtEqZero, coeff_mul_order_add_order, leadingCoeff_eq, addVal_apply_of_ne, min_order_le_order_add, coeff_order_eq_zero, order_of_ne, order_zero, order_eq_orderTop_of_ne_zero, order_smul_not_lt, order_eq_orderTop_of_ne, inv_def, order_pow, order_C, le_order_iff_forall, order_one, zero_lt_orderTop_iff, zero_le_orderTop_iff, order_mul_of_ne_zero, le_order_smul, order_single

LinearRecurrence

Definitions

Name	Category	Theorems
order 📖	CompOp	4 math math: sol_eq_of_eq_init, solSpace_rank, mkSol_eq_init, charPoly_degree_eq_order

MvPowerSeries

Definitions

Name	Category	Theorems
order 📖	CompOp	29 math math: le_order_mul, le_order_prod, nat_le_order, one_le_order_iff_constCoeff_eq_zero, le_order_subst, le_order, order_le, PowerSeries.order_eq_order, order_toSubring, le_order_smul, order_eq_top_iff, order_expand, PowerSeries.le_order_subst, order_mul_ge, ne_zero_iff_order_finite, order_monomial, order_neg, order_add_of_order_ne, PowerSeries.le_order_subst_right, order_prod, order_eq_nat, order_mul, order_zero, le_order_pow, min_order_le_add, order_monomial_of_ne_zero, le_order_pow_of_constantCoeff_eq_zero, PowerSeries.le_order_subst_left, le_order_map

PowerSeries

Definitions

Name	Category	Theorems
order 📖	CompOp	58 math math: le_order_subst_left', order_expand, degree_weierstrassMod_lt, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, order_mul_ge, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, le_order_smul, order_finite_iff_ne_zero, IsWeierstrassFactorization.isWeierstrassDivision, le_order_subst_right', IsWeierstrassDivisionAt.degree_lt, IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, le_order_map, order_monomial, le_order_mul, IsWeierstrassFactorization.natDegree_eq_toNat_order_map, order_zero, one_le_order_iff_constCoeff_eq_zero, coe_toNat_order, le_order_pow_of_constantCoeff_eq_zero, IsWeierstrassDivisorAt.isUnit_shift, order_eq_order, constantCoeff_divXPowOrder, min_order_le_order_add, order_exp, le_order_pow, order_pow, le_order_subst, order_prod, order_le, order_zero_of_unit, order_one, le_order, X_pow_order_dvd, coeff_divXPowOrder, order_toSubring, IsWeierstrassFactorization.degree_eq_coe_lift_order_map, coe_orderHom, IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, isWeierstrassDivisionAt_iff, order_neg, X_pow_order_mul_divXPowOrder, order_eq_top, order_X, order_eq, order_add_of_order_ne, order_eq_emultiplicity_X, order_mul, nat_le_order, IsWeierstrassDivisorAt.seq_one, order_X_pow, le_order_prod, order_add_of_order_eq, le_weightedOrder_subst, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, order_monomial_of_ne_zero, le_order_subst_left, order_eq_nat

---

← Back to Index