| Name | Category | Theorems |
|---|
acm 📖 | CompOp | 43 mathmath: degree_add_of_ne, degree_sub_le, degree_reduce_lt, zero_le, toSyn_strictMono, div_single, degree_add_le, le_degree, lex_lt_iff_of_unique, degLex_le_iff, bot_eq_zero, toSyn_lt_iff_ne_zero, degree_le_iff, degree_sum_le, degree_mul_lt_iff_left_lt_of_ne_zero, degree_smul_le, degree_mul_le, le_add_right, degree_pow_le, toSyn_monotone, degLex_single_le_iff, toSyn_eq_zero_iff, degree_prod_le, div_set, degLex_lt_iff, lex_lt_iff, eq_zero_iff, div, lex_le_iff, degree_sPolynomial_le, degree_sub_leadingTerm_lt_degree, degree_monomial_le, degLex_single_lt_iff, degree_sub_LTerm_lt, sPolynomial_lt_of_degree_ne_zero_of_degree_eq, degree_sPolynomial_lt_sup_degree, degree_sub_leadingTerm_lt_iff, degree_sub_leadingTerm_le, iocam, degree_sub_LTerm_le, lex_le_iff_of_unique, degree_sPolynomial, degree_X_le_single
|
lex 📖 | CompOp | 4 mathmath: lex_lt_iff_of_unique, lex_lt_iff, lex_le_iff, lex_le_iff_of_unique
|
lo 📖 | CompOp | 43 mathmath: degree_add_of_ne, degree_sub_le, degree_reduce_lt, zero_le, toSyn_strictMono, div_single, degree_add_le, le_degree, lex_lt_iff_of_unique, degLex_le_iff, bot_eq_zero, toSyn_lt_iff_ne_zero, degree_le_iff, degree_sum_le, degree_mul_lt_iff_left_lt_of_ne_zero, degree_smul_le, degree_mul_le, le_add_right, degree_pow_le, toSyn_monotone, degLex_single_le_iff, wf, degree_prod_le, div_set, degLex_lt_iff, lex_lt_iff, eq_zero_iff, div, lex_le_iff, degree_sPolynomial_le, degree_sub_leadingTerm_lt_degree, degree_monomial_le, degLex_single_lt_iff, degree_sub_LTerm_lt, sPolynomial_lt_of_degree_ne_zero_of_degree_eq, degree_sPolynomial_lt_sup_degree, degree_sub_leadingTerm_lt_iff, degree_sub_leadingTerm_le, iocam, degree_sub_LTerm_le, lex_le_iff_of_unique, degree_sPolynomial, degree_X_le_single
|
orderBot 📖 | CompOp | 2 mathmath: bot_eq_zero, degree_sum_le
|
syn 📖 | CompOp | 44 mathmath: degree_add_of_ne, degree_sub_le, degree_reduce_lt, zero_le, toSyn_strictMono, div_single, degree_add_le, le_degree, lex_lt_iff_of_unique, degLex_le_iff, bot_eq_zero, toSyn_lt_iff_ne_zero, degree_le_iff, degree_sum_le, degree_mul_lt_iff_left_lt_of_ne_zero, degree_smul_le, degree_mul_le, le_add_right, degree_pow_le, toSyn_monotone, degLex_single_le_iff, wf, toSyn_eq_zero_iff, degree_prod_le, div_set, degLex_lt_iff, lex_lt_iff, eq_zero_iff, div, lex_le_iff, degree_sPolynomial_le, degree_sub_leadingTerm_lt_degree, degree_monomial_le, degLex_single_lt_iff, degree_sub_LTerm_lt, sPolynomial_lt_of_degree_ne_zero_of_degree_eq, degree_sPolynomial_lt_sup_degree, degree_sub_leadingTerm_lt_iff, degree_sub_leadingTerm_le, iocam, degree_sub_LTerm_le, lex_le_iff_of_unique, degree_sPolynomial, degree_X_le_single
|
toSyn 📖 | CompOp | 38 mathmath: degree_add_of_ne, degree_sub_le, degree_reduce_lt, toSyn_strictMono, div_single, degree_add_le, le_degree, lex_lt_iff_of_unique, degLex_le_iff, degree_le_iff, degree_sum_le, degree_mul_lt_iff_left_lt_of_ne_zero, degree_smul_le, degree_mul_le, le_add_right, degree_pow_le, toSyn_monotone, degLex_single_le_iff, toSyn_eq_zero_iff, degree_prod_le, div_set, degLex_lt_iff, lex_lt_iff, div, lex_le_iff, degree_sPolynomial_le, degree_sub_leadingTerm_lt_degree, degree_monomial_le, degLex_single_lt_iff, degree_sub_LTerm_lt, sPolynomial_lt_of_degree_ne_zero_of_degree_eq, degree_sPolynomial_lt_sup_degree, degree_sub_leadingTerm_lt_iff, degree_sub_leadingTerm_le, degree_sub_LTerm_le, lex_le_iff_of_unique, degree_sPolynomial, degree_X_le_single
|
«term_≺[_]_» 📖 | CompOp | — |
«term_≼[_]_» 📖 | CompOp | — |