| Metric | Count |
|---|
DefinitionsAddMonoidAlgebra, addAddCommGroup, addAddCommMonoid, commRing, commSemiring, curryRingEquiv, distribSMul, inhabited, instCoeFun, instMul, nonAssocRing, nonAssocSemiring, nonUnitalCommRing, nonUnitalCommSemiring, nonUnitalNonAssocRing, nonUnitalNonAssocSemiring, nonUnitalRing, nonUnitalSemiring, of, of', ofMagma, semiring, single, singleAddHom, singleHom, singleZeroRingHom, smulZeroClass, unexpander, unique, uniqueRingEquiv, zero, «term__[_]», addCommGroup, addCommMonoid, commRing, commSemiring, curryRingEquiv, distribSMul, inhabited, instCoeFun, instMul, mul', nonAssocRing, nonAssocSemiring, nonUnitalCommRing, nonUnitalCommSemiring, nonUnitalNonAssocRing, nonUnitalNonAssocSemiring, nonUnitalRing, nonUnitalSemiring, of, ofMagma, one, semiring, single, singleAddHom, singleHom, singleOneRingHom, smulZeroClass, unexpander, unique, uniqueRingEquiv, «term__[_]» | 63 |
TheoremsaddHom_ext', addHom_ext'_iff, coe_add, coeff_smul, curryRingEquiv_single, curryRingEquiv_symm_single, ext, ext_iff, induction_linear, induction_on, instIsCancelAdd, intCast_def, isCentralScalar, isLocalHom_singleZeroRingHom, isScalarTower, mul_apply, mul_apply_antidiagonal, mul_apply_left, mul_apply_right, mul_def, mul_single_apply, mul_single_apply_aux, mul_single_apply_of_not_exists_add, mul_single_zero_apply, natCast_def, neg_apply, nontrivial, of'_apply, of'_commute, of'_eq_of, ofMagma_apply, of_apply, of_injective, one_def, prod_single, ringHom_ext, ringHom_ext', ringHom_ext'_iff, singleAddHom_apply, singleHom_apply, singleZeroRingHom_apply, single_add, single_apply, single_commute, single_commute_single, single_eq_zero, single_mul_apply, single_mul_apply_aux, single_mul_apply_of_not_exists_add, single_mul_single, single_ne_zero, single_neg, single_pow, single_zero, single_zero_comm, single_zero_mul_apply, smulCommClass, smul_single, smul_single', sum_single, sum_single_index, uniqueRingEquiv_apply, uniqueRingEquiv_symm_apply, addHom_ext', addHom_ext'_iff, coe_add, curryRingEquiv_single, curryRingEquiv_symm_single, ext, ext_iff, induction_linear, induction_on, instIsCancelAdd, intCast_def, isCentralScalar, isLocalHom_singleOneRingHom, isScalarTower, mul_apply, mul_apply_antidiagonal, mul_apply_left, mul_apply_right, mul_def, mul_single_apply, mul_single_apply_aux, mul_single_apply_of_not_exists_mul, mul_single_one_apply, natCast_def, neg_apply, nontrivial, ofMagma_apply, of_apply, of_commute, of_injective, one_def, prod_single, ringHom_ext, ringHom_ext', ringHom_ext'_iff, singleAddHom_apply, singleHom_apply, singleOneRingHom_apply, single_add, single_apply, single_commute, single_commute_single, single_eq_zero, single_mul_apply, single_mul_apply_aux, single_mul_apply_of_not_exists_mul, single_mul_single, single_ne_zero, single_neg, single_one_comm, single_one_mul_apply, single_pow, single_zero, smulCommClass, smul_apply, smul_single, smul_single', sum_single, sum_single_index, uniqueRingEquiv_apply, uniqueRingEquiv_symm_apply | 124 |
| Total | 187 |
| Name | Category | Theorems |
|---|
addAddCommGroup 📖 | CompOp | 10 mathmath: DirectSum.toAddMonoidAlgebra_sub, neg_apply, supDegree_neg, Polynomial.ofFinsupp_neg, Polynomial.toFinsupp_neg, toDirectSum_sub, supDegree_sub_le, toDirectSum_neg, single_neg, DirectSum.toAddMonoidAlgebra_neg
|
addAddCommMonoid 📖 | CompOp | 98 mathmath: supDegree_sum_lt, liftNC_mul, of'_mem_span, LaurentPolynomial.comul_T, le_infDegree_add, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, comul_single, isScalarTower_self, supDegree_add_le, divOfHom_apply_apply, Polynomial.eval₂_ofFinsupp, singleZeroRingHom_apply, instIsTorsionFree, counit_single, smulCommClass, moduleFinite, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, decomposeAux_coe, lsingle_apply, gradeBy.isInternal, single_add, smul_single, tensorEquiv.invFun_tmul, smulCommClass_symm_self, le_inf_support_add, isScalarTower, mul_def, toDirectSum_zero, toDirectSum_add, coe_add, leadingCoeff_zero, Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp, LaurentPolynomial.leval_apply, faithfulSMul, GradesBy.decompose_single, singleAddHom_apply, coe_liftNCAlgHom, Polynomial.ofFinsupp_smul, mem_grade_iff', coeff_smul, DirectSum.toAddMonoidAlgebra_zero, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, single_mem_grade, Polynomial.toFinsuppIsoLinear_apply, LaurentPolynomial.comul_C, liftNC_smul, liftNC_single, smul_single', supDegree_leadingCoeff_sum_eq, tensorEquiv_tmul, gradeBy.gradedMonoid, tensorEquiv_symm_single, mem_grade_iff, grade.decompose_single, single_eq_zero, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, lhom_ext'_iff, single_zero, Polynomial.toFinsupp_sum, LaurentPolynomial.counit_C_mul_T, basis_apply, DirectSum.toAddMonoidAlgebra_add, grade.isInternal, Polynomial.toFinsupp_smul, mapDomain_zero, liftNC_one, scalarTensorEquiv_symm_single, sup_support_add_le, instIsCocomm, instFree, LaurentPolynomial.instIsCocomm, LaurentPolynomial.counit_T, LaurentPolynomial.counit_C, LaurentPolynomial.comul_C_mul_T, mem_span_support', LaurentPolynomial.smul_eq_C_mul, decomposeAux_single, addHom_ext'_iff, addMonoidAlgebraAddEquivDirectSum_symm_apply, decomposeAux_eq_decompose, mapDomain_add, lift_def, instIsCancelAdd, addMonoidAlgebraAddEquivDirectSum_apply, scalarTensorEquiv_tmul, distribMulActionHom_ext'_iff, Polynomial.ofFinsupp_sum, sum_single, single_mem_gradeBy, grade.gradedMonoid, isCentralScalar, LaurentPolynomial.comul_C_mul_T_self, LaurentPolynomial.instIsScalarTowerPolynomial, smulCommClass_self, mem_gradeBy_iff, mapDomain_sum, mem_span_support, supDegree_sum_le
|
commRing 📖 | CompOp | 2 mathmath: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe
|
commSemiring 📖 | CompOp | 16 mathmath: LaurentPolynomial.mk'_one_X_pow, LaurentPolynomial.mk'_mul_T, LaurentPolynomial.mk'_one_X, algebraMap_def, mvPolynomial_aeval_of_surjective_of_closure, sup_support_multiset_prod_le, prod_single, LaurentPolynomial.mk'_eq, instIsPushout, instIsPushout', sup_support_finset_prod_le, LaurentPolynomial.isLocalization, le_inf_support_finset_prod, le_inf_support_multiset_prod, supDegree_prod_le, vaddAssocClass_addMonoidAlgebra
|
curryRingEquiv 📖 | CompOp | 2 mathmath: curryRingEquiv_symm_single, curryRingEquiv_single
|
distribSMul 📖 | CompOp | — |
inhabited 📖 | CompOp | — |
instCoeFun 📖 | CompOp | — |
instMul 📖 | CompOp | 111 mathmath: sup_support_list_prod_le, instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums, instIsCancelAddZeroOfIsCancelAddOfUniqueSums, mul_single_apply, LaurentPolynomial.degree_C_mul_T_ite, mapDomainRingEquiv_apply, mul_apply, LaurentPolynomial.mk'_mul_T, liftNC_mul, LaurentPolynomial.mul_T_assoc, LaurentPolynomial.commute_T, LaurentPolynomial.T_sub, Monic.supDegree_mul, Monic.supDegree_mul_of_ne_zero_right, instNoZeroDivisorsOfUniqueSums, instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums, uniqueRingEquiv_apply, opRingEquiv_symm_single, opRingEquiv_symm_apply, LaurentPolynomial.eval₂_C_mul_T, Polynomial.toLaurent_C_mul_T, LaurentPolynomial.invOf_T, supDegree_mul, LaurentPolynomial.smeval_C_mul, of'_commute, single_commute_single, of'_mul_divOf, mapRangeRingEquiv_trans, Monic.leadingCoeff_mul_eq_left, LaurentPolynomial.degree_C_mul_T, support_mul_single_subset, Monic.mul, support_single_mul_subset, toDirectSum_mul, mul_def, LaurentPolynomial.mk'_eq, Monic.leadingCoeff_mul_eq_right, apply_add_of_supDegree_le, DirectSum.toAddMonoidAlgebra_mul, commRingEquiv_single_single, mul_of'_modOf, mul_single_zero_apply, le_inf_support_list_prod, mapDomainRingEquiv_trans, support_mul_single_eq_image, mul_apply_left, single_zero_comm, modOf_add_divOf, LaurentPolynomial.eval₂_C_mul_T_neg_n, support_mul, Polynomial.toFinsupp_mul, single_mul_apply, single_mul_apply_of_not_exists_add, LaurentPolynomial.single_eq_C_mul_T, opRingEquiv_single, ofMagma_apply, mul_single_apply_aux, sup_support_mul_le, mul_apply_add_eq_mul_of_uniqueAdd, single_mul_single, le_infDegree_mul, le_inf_support_mul, curryRingEquiv_symm_single, opRingEquiv_apply, mapDomainRingEquiv_single, Monic.supDegree_mul_of_ne_zero_left, Polynomial.toFinsuppIso_apply, uniqueRingEquiv_symm_apply, leadingCoeff_mul, mapDomain_mul, symm_mapDomainRingEquiv, LaurentPolynomial.counit_C_mul_T, mapRangeRingEquiv_apply, supDegree_mul_le, divOf_add_modOf, Polynomial.ofFinsupp_mul, support_single_mul, support_single_mul_eq_image, LaurentPolynomial.support_C_mul_T_of_ne_zero, single_zero_mul_apply, LaurentPolynomial.comul_C_mul_T, LaurentPolynomial.smeval_C_mul_T_n, single_mul_apply_aux, Polynomial.toFinsuppIso_symm_apply, LaurentPolynomial.smul_eq_C_mul, Polynomial.toLaurent_C_mul_eq, curryRingEquiv_single, addMonoidAlgebraRingEquivDirectSum_apply, LaurentPolynomial.trunc_C_mul_T, LaurentPolynomial.support_C_mul_T, addMonoidAlgebraRingEquivDirectSum_symm_apply, symm_mapRangeRingEquiv, of'_mul_modOf, symm_commRingEquiv, Polynomial.toLaurent_C_mul_X_pow, LaurentPolynomial.eval₂_C_mul_T_n, LaurentPolynomial.toLaurent_reverse, single_commute, LaurentPolynomial.comul_C_mul_T_self, mul_apply_right, LaurentPolynomial.T_add, LaurentPolynomial.exists_T_pow, mul_single_apply_of_not_exists_add, mapRangeRingEquiv_single, support_mul_single, LaurentPolynomial.antipode_C_mul_T, mul_apply_antidiagonal, LaurentPolynomial.degree_C_mul_T_le, LaurentPolynomial.T_mul, apply_supDegree_add_supDegree, mul_of'_divOf
|
nonAssocRing 📖 | CompOp | 2 mathmath: intCast_def, supDegree_sub_lt_of_leadingCoeff_eq
|
nonAssocSemiring 📖 | CompOp | 92 mathmath: singleHom_apply, LaurentPolynomial.degree_C_mul_T_ite, Polynomial.toLaurent_eq_zero, algHom_ext'_iff, LaurentPolynomial.mk'_mul_T, liftNCRingHom_single, toRingHom_mapRangeRingEquiv, toRingHom_mapDomainRingEquiv, lift_mapRangeRingHom_algebraMap, divOfHom_apply_apply, Polynomial.trunc_toLaurent, mapRangeRingHom_comp_algebraMap, Polynomial.ofFinsupp_natCast, LaurentPolynomial.eval₂_C_mul_T, Polynomial.toLaurent_C_mul_T, singleZeroRingHom_apply, LaurentPolynomial.algebraMap_apply, mapRangeRingHom_single, mapDomainRingHom_comp_algebraMap, LaurentPolynomial.smeval_C_mul, Polynomial.toLaurent_injective, of_apply, LaurentPolynomial.degree_C_mul_T, mapRangeRingHom_apply, LaurentPolynomial.smeval_C, isLocalHom_singleZeroRingHom, ringHom_ext'_iff, LaurentPolynomial.degree_C, LaurentPolynomial.eval₂_T, LaurentPolynomial.C_apply, Polynomial.toFinsupp_nsmul, Polynomial.toLaurent_comp_C, LaurentPolynomial.mk'_eq, mapRangeRingHom_comp, toDirectSum_natCast, Polynomial.toLaurent_apply, DirectSum.toAddMonoidAlgebra_natCast, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, Polynomial.toFinsupp_natCast, mapDomainRingHom_comp, LaurentPolynomial.single_eq_C, natCast_def, LaurentPolynomial.eval₂_C_mul_T_neg_n, lift_of, coe_mapRangeRingHom, LaurentPolynomial.C_eq_algebraMap, LaurentPolynomial.single_eq_C_mul_T, LaurentPolynomial.comul_C, LaurentPolynomial.eval₂_C, LaurentPolynomial.eval₂_toLaurent, lift_unique', toRingHom_mapRangeAlgHom, LaurentPolynomial.toLaurent_support, Polynomial.toLaurent_inj, LaurentPolynomial.counit_C_mul_T, Polynomial.toLaurent_one, LaurentPolynomial.degree_C_ite, LaurentPolynomial.eval₂_T_neg_n, LaurentPolynomial.antipode_C, of_injective, mapRangeRingHom_id, LaurentPolynomial.support_C_mul_T_of_ne_zero, LaurentPolynomial.counit_C, LaurentPolynomial.comul_C_mul_T, LaurentPolynomial.smeval_C_mul_T_n, LaurentPolynomial.leftInverse_trunc_toLaurent, LaurentPolynomial.smul_eq_C_mul, Polynomial.toLaurent_C_mul_eq, LaurentPolynomial.eval₂_T_n, LaurentPolynomial.trunc_C_mul_T, LaurentPolynomial.support_C_mul_T, Polynomial.toLaurent_X, mapDomainRingHom_id, Polynomial.coe_toLaurentAlg, Polynomial.toLaurent_C, Polynomial.toLaurentAlg_apply, Polynomial.toLaurent_C_mul_X_pow, LaurentPolynomial.eval₂_C_mul_T_n, LaurentPolynomial.toLaurent_reverse, of'_eq_of, LaurentPolynomial.comul_C_mul_T_self, LaurentPolynomial.instIsScalarTowerPolynomial, LaurentPolynomial.invert_C, Polynomial.ofFinsupp_nsmul, LaurentPolynomial.exists_T_pow, mapRangeRingHom_comp_mapDomainRingHom, LaurentPolynomial.invert_comp_C, LaurentPolynomial.antipode_C_mul_T, LaurentPolynomial.degree_C_le, mapDomainRingHom_apply, LaurentPolynomial.degree_C_mul_T_le
|
nonUnitalCommRing 📖 | CompOp | — |
nonUnitalCommSemiring 📖 | CompOp | — |
nonUnitalNonAssocRing 📖 | CompOp | — |
nonUnitalNonAssocSemiring 📖 | CompOp | 69 mathmath: instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums, instIsCancelAddZeroOfIsCancelAddOfUniqueSums, mapDomainRingEquiv_apply, Polynomial.toLaurent_eq_zero, Polynomial.ofFinsupp_zero, mapDomainNonUnitalRingHom_id, isScalarTower_self, mapRangeAddEquiv_apply, mapDomainAddEquiv_single, zero_divOf, mapDomainNonUnitalAlgHom_apply, mapDomainAddEquiv_apply, instNoZeroDivisorsOfUniqueSums, instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums, uniqueRingEquiv_apply, opRingEquiv_symm_single, opRingEquiv_symm_apply, mapRangeRingEquiv_trans, mapRangeAddEquiv_trans, supDegree_add_eq_right, smulCommClass_symm_self, Polynomial.toFinsupp_eq_zero, Polynomial.ofFinsupp_add, leadingCoeff_add_eq_right, supDegree_zero, mapDomainNonUnitalRingHom_apply, leadingCoeff_eq_zero, leadingCoeff_add_eq_left, of'_dvd_iff_modOf_eq_zero, commRingEquiv_single_single, mul_of'_modOf, add_divOf, mapDomainRingEquiv_trans, modOf_add_divOf, nonUnitalAlgHom_ext'_iff, liftMagma_apply_apply, mapDomainNonUnitalRingHom_comp, opRingEquiv_single, liftMagma_symm_apply, curryRingEquiv_symm_single, opRingEquiv_apply, mapDomainRingEquiv_single, Polynomial.toFinsuppIso_apply, uniqueRingEquiv_symm_apply, symm_mapDomainRingEquiv, supDegree_add_eq_left, Polynomial.toFinsupp_add, mapRangeRingEquiv_apply, divOf_add_modOf, mapRangeAddEquiv_single, Polynomial.toFinsuppIso_symm_apply, LaurentPolynomial.degree_eq_bot_iff, mapDomainAddEquiv_trans, curryRingEquiv_single, Polynomial.ofFinsupp_eq_zero, addMonoidAlgebraRingEquivDirectSum_apply, addMonoidAlgebraRingEquivDirectSum_symm_apply, symm_mapRangeRingEquiv, of'_mul_modOf, LaurentPolynomial.smeval_zero, of'_modOf, symm_commRingEquiv, symm_mapDomainAddEquiv, LaurentPolynomial.smeval_add, Polynomial.toFinsupp_zero, smulCommClass_self, LaurentPolynomial.degree_zero, mapRangeRingEquiv_single, symm_mapRangeAddEquiv
|
nonUnitalRing 📖 | CompOp | — |
nonUnitalSemiring 📖 | CompOp | 1 mathmath: of'_dvd_iff_modOf_eq_zero
|
of 📖 | CompOp | 7 mathmath: algHom_ext'_iff, of_apply, ringHom_ext'_iff, lift_of, lift_unique', of_injective, of'_eq_of
|
of' 📖 | CompOp | 23 mathmath: of'_mem_span, of'_divOf, of'_commute, of'_mul_divOf, mvPolynomial_aeval_of_surjective_of_closure, mem_ideal_span_of'_image, of'_dvd_iff_modOf_eq_zero, mul_of'_modOf, modOf_add_divOf, exists_finset_adjoin_eq_top, of'_apply, lift_of', mem_adjoin_support, divOf_add_modOf, support_gen_of_gen, mem_span_support', of'_mul_modOf, of'_modOf, support_gen_of_gen', of'_eq_of, mem_span_support, freeAlgebra_lift_of_surjective_of_closure, mul_of'_divOf
|
ofMagma 📖 | CompOp | 3 mathmath: nonUnitalAlgHom_ext'_iff, ofMagma_apply, liftMagma_symm_apply
|
semiring 📖 | CompOp | 104 mathmath: mapRangeAlgEquiv_trans, lift_apply', domCongr_comp_lsingle, symm_mapRangeAlgEquiv, algHom_ext'_iff, mapRangeAlgHom_single, Polynomial.toFinsupp_pow, domCongr_toAlgHom, lift_mapRangeRingHom_algebraMap, LaurentPolynomial.T_pow, mapDomainBialgHom_id, mapDomainAlgHom_id, mapRangeRingHom_comp_algebraMap, algebraMap_def, LaurentPolynomial.algebraMap_apply, LaurentPolynomial.antipode_T, mapDomainRingHom_comp_algebraMap, Monic.pow, mapDomainBialgHom_mapDomainBialgHom, BoundedContinuousFunction.charAlgHom_apply, domCongr_refl, decomposeAux_coe, Polynomial.ofFinsupp_pow, tensorEquiv.invFun_tmul, Polynomial.ofFinsupp_algebraMap, isLocalHom_singleZeroRingHom, commAlgEquiv_single_single, isLocalHom_algebraMap, lift_apply, mem_ideal_span_of'_image, domCongr_single, mapDomainBialgHom_apply, coe_algebraMap, le_inf_support_pow, mapRangeAlgEquiv_apply, finiteType_of_fg, addMonoidAlgebraAlgEquivDirectSum_symm_apply, commRingEquiv_single_single, LaurentPolynomial.algebraMap_X_pow, finiteType_iff_group_fg, LaurentPolynomial.algebraMap_eq_toLaurent, toDirectSum_pow, lift_single, mapDomainAlgHom_apply, lift_symm_apply, LaurentPolynomial.isUnit_T, coe_liftNCAlgHom, lift_of, LaurentPolynomial.C_eq_algebraMap, mapDomain_algebraMap, exists_finset_adjoin_eq_top, lift_unique', toRingHom_mapRangeAlgHom, tensorEquiv_tmul, gradeBy.gradedMonoid, Polynomial.toFinsupp_algebraMap, LaurentPolynomial.invert_symm, symm_commAlgEquiv, mapDomainAlgHom_comp, tensorEquiv_symm_single, lift_of', curryRingEquiv_symm_single, mem_adjoin_support, Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp, domCongr_support, Monic.supDegree_pow, curryAlgEquiv_symm_single, domCongr_symm, algHom_ext_iff, sup_support_pow_le, LaurentPolynomial.invert_apply, mapDomainBialgHom_comp, LaurentPolynomial.antipode_C, scalarTensorEquiv_symm_single, Polynomial.toFinsuppIsoAlg_apply, finiteType_iff_fg, single_pow, domCongr_apply, decomposeAux_single, curryRingEquiv_single, DirectSum.toAddMonoidAlgebra_pow, antipode_single, decomposeAux_eq_decompose, lift_unique, lift_def, singleZeroAlgHom_apply, Polynomial.coe_toLaurentAlg, scalarTensorEquiv_tmul, Polynomial.toLaurentAlg_apply, symm_commRingEquiv, LaurentPolynomial.toLaurent_reverse, addMonoidAlgebraAlgEquivDirectSum_apply, grade.gradedMonoid, isLocalHom_singleZeroAlgHom, LaurentPolynomial.invert_C, curryAlgEquiv_single, mapRangeAlgHom_apply, LaurentPolynomial.invert_comp_C, LaurentPolynomial.antipode_C_mul_T, freeAlgebra_lift_of_surjective_of_closure, instIsDomainOfIsCancelAddOfUniqueSums, LaurentPolynomial.invert_T, vaddAssocClass_addMonoidAlgebra, LaurentPolynomial.involutive_invert
|
single 📖 | CompOp | 87 mathmath: singleHom_apply, mul_single_apply, liftNCRingHom_single, supDegree_single, comul_single, mapRangeAlgHom_single, mapDomainAddEquiv_single, Polynomial.toFinsupp_monomial, single_apply, opRingEquiv_symm_single, intCast_def, counit_single, mapRangeRingHom_single, toDirectSum_single, single_commute_single, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, Polynomial.ofFinsupp_single, lsingle_apply, of_apply, single_add, smul_single, support_mul_single_subset, commAlgEquiv_single_single, support_single_mul_subset, domCongr_single, Polynomial.toFinsupp_X_pow, prod_single, mul_def, coe_algebraMap, commRingEquiv_single_single, mul_single_zero_apply, lift_single, lift_symm_apply, support_mul_single_eq_image, LaurentPolynomial.single_eq_C, single_zero_comm, singleAddHom_apply, natCast_def, leadingCoeff_single, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, single_mul_apply, single_mul_apply_of_not_exists_add, LaurentPolynomial.single_eq_C_mul_T, of'_apply, liftNC_single, opRingEquiv_single, smul_single', ofMagma_apply, mul_single_apply_aux, Polynomial.toFinsupp_X, single_mul_single, tensorEquiv_symm_single, DirectSum.toAddMonoidAlgebra_of, curryRingEquiv_symm_single, mapDomainRingEquiv_single, single_eq_zero, LaurentPolynomial.smeval_single, single_zero, curryAlgEquiv_symm_single, algHom_ext_iff, basis_apply, LaurentPolynomial.single_zero_one_eq_one, scalarTensorEquiv_symm_single, support_single_mul, support_single_mul_eq_image, single_pow, single_zero_mul_apply, supDegree_single_ne_zero, mapRangeAddEquiv_single, Polynomial.toFinsupp_C_mul_X_pow, single_neg, single_mul_apply_aux, curryRingEquiv_single, Polynomial.toFinsupp_C_mul_X, antipode_single, lift_unique, singleZeroAlgHom_apply, mapDomain_single, sum_single, single_commute, sum_single_index, curryAlgEquiv_single, mul_single_apply_of_not_exists_add, one_def, mapRangeRingEquiv_single, support_mul_single, Polynomial.toFinsupp_C
|
singleAddHom 📖 | CompOp | 3 mathmath: singleZeroRingHom_apply, singleAddHom_apply, addHom_ext'_iff
|
singleHom 📖 | CompOp | 1 mathmath: singleHom_apply
|
singleZeroRingHom 📖 | CompOp | 3 mathmath: singleZeroRingHom_apply, isLocalHom_singleZeroRingHom, ringHom_ext'_iff
|
smulZeroClass 📖 | CompOp | 14 mathmath: isScalarTower_self, smulCommClass, smul_single, smulCommClass_symm_self, isScalarTower, faithfulSMul, Polynomial.ofFinsupp_smul, coeff_smul, liftNC_smul, smul_single', Polynomial.toFinsupp_smul, LaurentPolynomial.smul_eq_C_mul, isCentralScalar, smulCommClass_self
|
unexpander 📖 | CompOp | — |
unique 📖 | CompOp | — |
uniqueRingEquiv 📖 | CompOp | 2 mathmath: uniqueRingEquiv_apply, uniqueRingEquiv_symm_apply
|
zero 📖 | CompOp | 20 mathmath: sup_support_list_prod_le, of'_divOf, mapDomain_one, LaurentPolynomial.invOf_T, DirectSum.toAddMonoidAlgebra_one, LaurentPolynomial.T_zero, Polynomial.ofFinsupp_eq_one, Polynomial.ofFinsupp_one, le_inf_support_list_prod, Polynomial.toFinsupp_one, monic_one, support_one_subset, Polynomial.toFinsupp_eq_one, Polynomial.toLaurent_one, LaurentPolynomial.smeval_one, LaurentPolynomial.single_zero_one_eq_one, liftNC_one, toDirectSum_one, one_def, support_one
|
«term__[_]» 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
addCommGroup 📖 | CompOp | 5 mathmath: FreeLieAlgebra.Rel.neg, FreeLieAlgebra.Rel.subRight, FreeLieAlgebra.Rel.subLeft, single_neg, neg_apply
|
addCommMonoid 📖 | CompOp | 52 mathmath: Representation.ofMulActionSelfAsModuleEquiv_symm_apply, instIsCocomm, tensorEquiv.invFun_tmul, liftNC_mul, mul_def, instIsCancelAdd, single_eq_zero, smulCommClass, of_mem_span_of_iff, coe_liftNCAlgHom, smulCommClass_self, distribMulActionHom_ext'_iff, FreeLieAlgebra.liftAux_map_smul, scalarTensorEquiv_tmul, instFree, basis_apply, AddMonoidAlgebra.tensorEquiv.invFun_tmul, singleAddHom_apply, mem_span_support, faithfulSMul, lsingle_apply, tensorEquiv_symm_single, smul_single, coe_add, moduleFinite, smul_of, Representation.ofMulActionSelfAsModuleEquiv_apply, liftNC_single, smul_single', tensorEquiv_tmul, sum_single, smul_apply, lhom_ext'_iff, scalarTensorEquiv_symm_single, comul_single, singleOneRingHom_apply, smulCommClass_symm_self, mapDomain_zero, FreeLieAlgebra.Rel.smulOfTower, single_zero, liftNC_smul, instIsTorsionFree, single_add, isScalarTower_self, lift_def, isCentralScalar, isScalarTower, addHom_ext'_iff, mapDomain_sum, liftNC_one, counit_single, mapDomain_add
|
commRing 📖 | CompOp | 2 mathmath: CommRingCat.monoidAlgebra_map, CommRingCat.monoidAlgebra_obj
|
commSemiring 📖 | CompOp | 6 mathmath: instIsPushout, mvPolynomial_aeval_of_surjective_of_closure, isScalarTower_monoidAlgebra, instIsPushout', algebraMap_def, prod_single
|
curryRingEquiv 📖 | CompOp | 2 mathmath: curryRingEquiv_symm_single, curryRingEquiv_single
|
distribSMul 📖 | CompOp | — |
inhabited 📖 | CompOp | — |
instCoeFun 📖 | CompOp | — |
instMul 📖 | CompOp | 56 mathmath: mapDomainRingEquiv_single, liftNC_mul, mul_def, opRingEquiv_single, mapDomainRingEquiv_trans, single_one_mul_apply, opRingEquiv_symm_apply, uniqueRingEquiv_apply, mapRangeRingEquiv_single, single_mul_apply, single_algebraMap_eq_algebraMap_mul_of, symm_mapRangeRingEquiv, support_mul_single_eq_image, single_mul_apply_aux, ofMagma_apply, symm_commRingEquiv, opRingEquiv_symm_single, curryRingEquiv_symm_single, FreeLieAlgebra.liftAux_map_mul, mul_apply_mul_eq_mul_of_uniqueMul, single_mul_single, support_mul_single_subset, instIsCancelMulZeroOfIsCancelAddOfUniqueProds, single_commute, instNoZeroDivisorsOfUniqueProds, single_one_comm, mapRangeRingEquiv_apply, instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds, support_mul_single, mul_single_apply_of_not_exists_mul, mul_single_one_apply, mapRangeRingEquiv_trans, support_single_mul_eq_image, curryRingEquiv_single, of_commute, uniqueRingEquiv_symm_apply, support_single_mul, mul_apply, mapDomainRingEquiv_apply, instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds, single_commute_single, single_eq_algebraMap_mul_of, GroupAlgebra.mul_average_left, mul_apply_right, symm_mapDomainRingEquiv, mul_single_apply, support_single_mul_subset, mul_apply_antidiagonal, mapDomain_mul, single_mul_apply_of_not_exists_mul, support_mul, opRingEquiv_apply, commRingEquiv_single_single, GroupAlgebra.mul_average_right, mul_single_apply_aux, mul_apply_left
|
mul' 📖 | CompOp | — |
nonAssocRing 📖 | CompOp | 1 mathmath: intCast_def
|
nonAssocSemiring 📖 | CompOp | 47 mathmath: Representation.ofMulActionSelfAsModuleEquiv_symm_apply, mapRangeRingHom_single, algHom_ext'_iff, mapDomainRingHom_id, mem_adjoin_support, of_mem_span_of_iff, support_gen_of_gen', LinearMap.sumOfConjugatesEquivariant_apply, mvPolynomial_aeval_of_surjective_of_closure, toRingHom_mapRangeAlgHom, single_algebraMap_eq_algebraMap_mul_of, liftNCRingHom_single, mem_span_support, coe_mapRangeRingHom, isLocalHom_singleOneRingHom, mapRangeRingHom_comp_mapDomainRingHom, freeAlgebra_lift_of_surjective_of_closure, ringHom_ext_iff, mapRangeRingHom_comp_algebraMap, toRingHom_mapDomainRingEquiv, exists_finset_adjoin_eq_top, smul_of, Representation.ofMulActionSelfAsModuleEquiv_apply, Representation.asModuleEquiv_symm_map_rho, Representation.asAlgebraHom_of, singleHom_apply, support_gen_of_gen, LinearMap.equivariantProjection_apply, of_commute, mem_ideal_span_of_image, lift_mapRangeRingHom_algebraMap, of_injective, mapDomainRingHom_comp, equivariantOfLinearOfComm_apply, singleOneRingHom_apply, toRingHom_mapRangeRingEquiv, ringHom_ext'_iff, single_eq_algebraMap_mul_of, mapRangeRingHom_id, mapDomainRingHom_apply, mapDomainRingHom_comp_algebraMap, natCast_def, mapRangeRingHom_comp, of_apply, lift_of, mapRangeRingHom_apply, lift_unique'
|
nonUnitalCommRing 📖 | CompOp | — |
nonUnitalCommSemiring 📖 | CompOp | — |
nonUnitalNonAssocRing 📖 | CompOp | — |
nonUnitalNonAssocSemiring 📖 | CompOp | 51 mathmath: mapDomainRingEquiv_single, liftMagma_apply_apply, opRingEquiv_single, mapDomainRingEquiv_trans, FreeNonUnitalNonAssocAlgebra.of_comp_lift, opRingEquiv_symm_apply, FreeLieAlgebra.Rel.addLeft, symm_mapDomainAddEquiv, uniqueRingEquiv_apply, mapDomainNonUnitalRingHom_id, smulCommClass_self, FreeNonUnitalNonAssocAlgebra.lift_unique, mapDomainAddEquiv_single, mapRangeRingEquiv_single, FreeLieAlgebra.liftAux_map_smul, symm_mapRangeRingEquiv, symm_commRingEquiv, FreeLieAlgebra.liftAux_map_add, FreeNonUnitalNonAssocAlgebra.lift_symm_apply, opRingEquiv_symm_single, curryRingEquiv_symm_single, mapRangeAddEquiv_apply, FreeLieAlgebra.liftAux_map_mul, mapDomainAddEquiv_trans, mapRangeAddEquiv_trans, instIsCancelMulZeroOfIsCancelAddOfUniqueProds, FreeLieAlgebra.liftAux_spec, symm_mapRangeAddEquiv, instNoZeroDivisorsOfUniqueProds, mapRangeRingEquiv_apply, nonUnitalAlgHom_ext'_iff, mapDomainNonUnitalRingHom_apply, instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds, liftMagma_symm_apply, mapRangeRingEquiv_trans, curryRingEquiv_single, uniqueRingEquiv_symm_apply, mapDomainNonUnitalAlgHom_apply, mapDomainNonUnitalRingHom_comp, smulCommClass_symm_self, mapDomainRingEquiv_apply, instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds, mapRangeAddEquiv_single, isScalarTower_self, symm_mapDomainRingEquiv, mapDomainAddEquiv_apply, FreeNonUnitalNonAssocAlgebra.lift_of_apply, opRingEquiv_apply, commRingEquiv_single_single, FreeNonUnitalNonAssocAlgebra.hom_ext_iff, FreeNonUnitalNonAssocAlgebra.lift_comp_of
|
nonUnitalRing 📖 | CompOp | — |
nonUnitalSemiring 📖 | CompOp | — |
of 📖 | CompOp | 21 mathmath: algHom_ext'_iff, mem_adjoin_support, of_mem_span_of_iff, support_gen_of_gen', mvPolynomial_aeval_of_surjective_of_closure, single_algebraMap_eq_algebraMap_mul_of, mem_span_support, freeAlgebra_lift_of_surjective_of_closure, exists_finset_adjoin_eq_top, smul_of, Representation.asModuleEquiv_symm_map_rho, Representation.asAlgebraHom_of, support_gen_of_gen, of_commute, mem_ideal_span_of_image, of_injective, ringHom_ext'_iff, single_eq_algebraMap_mul_of, of_apply, lift_of, lift_unique'
|
ofMagma 📖 | CompOp | 3 mathmath: ofMagma_apply, nonUnitalAlgHom_ext'_iff, liftMagma_symm_apply
|
one 📖 | CompOp | 5 mathmath: support_one_subset, mapDomain_one, one_def, liftNC_one, support_one
|
semiring 📖 | CompOp | 102 mathmath: finiteType_of_fg, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, isLocalHom_algebraMap, Submodule.exists_isCompl, Representation.asAlgebraHom_single, algHom_ext'_iff, tensorEquiv.invFun_tmul, antipode_single, Subrepresentation.mem_ofSubmodule'_iff, domCongr_toAlgHom, Rep.to_Module_monoidAlgebra_map_aux, mem_adjoin_support, Representation.asAlgebraHom_def, lift_symm_apply, coe_liftNCAlgHom, Representation.smul_ofModule_asModule, LinearMap.sumOfConjugatesEquivariant_apply, mapDomainBialgHom_comp, coe_algebraMap, mapDomain_algebraMap, Representation.ofMulAction_self_smul_eq_mul, mapDomainBialgHom_mapDomainBialgHom, Representation.single_smul, mapRangeAlgHom_single, mapRangeAlgEquiv_trans, domCongr_single, toRingHom_mapRangeAlgHom, scalarTensorEquiv_tmul, single_algebraMap_eq_algebraMap_mul_of, mapDomainAlgHom_id, mapDomainAlgHom_comp, isLocalHom_singleOneRingHom, Subrepresentation.mem_asSubmodule'_iff, Representation.asModuleEquiv_symm_map_smul, mapRangeAlgHom_apply, symm_mapRangeAlgEquiv, lift_unique, tensorEquiv_symm_single, symm_commRingEquiv, lift_apply', Subrepresentation.submoduleSubrepresentationOrderIso_apply, mapDomainBialgHom_apply, mapRangeAlgEquiv_apply, freeAlgebra_lift_of_surjective_of_closure, Representation.asAlgebraHom_single_one, mapRangeRingHom_comp_algebraMap, Representation.isSimpleModule_iff_irreducible_ofModule, Representation.instIsScalarTowerMonoidAlgebraAsModule, curryRingEquiv_symm_single, Subrepresentation.mem_asSubmodule_iff, commAlgEquiv_single_single, isScalarTower_monoidAlgebra, isLocalHom_singleOneAlgHom, finiteType_iff_fg, exists_finset_adjoin_eq_top, Representation.ofMulActionSelfAsModuleEquiv_apply, LinearMap.conjugate_apply, Representation.asModuleEquiv_symm_map_rho, Representation.ofModule_asModule_act, tensorEquiv_tmul, Representation.asAlgebraHom_of, finiteType_iff_group_fg, domCongr_comp_lsingle, domCongr_symm, LinearMap.equivariantProjection_apply, GroupSMul.linearMap_apply, curryRingEquiv_single, scalarTensorEquiv_symm_single, Representation.smul_tprod_one_asModule, algebraMap_def, mem_ideal_span_of_image, lift_apply, lift_mapRangeRingHom_algebraMap, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, Representation.ofModule_asAlgebraHom_apply_apply, symm_commAlgEquiv, curryAlgEquiv_symm_single, single_eq_algebraMap_mul_of, single_pow, domCongr_support, Representation.asModuleEquiv_map_smul, singleOneAlgHom_apply, lift_def, Representation.smul_one_tprod_asModule, Representation.is_simple_module_iff_irreducible_ofModule, Subrepresentation.mem_ofSubmodule_iff, Representation.free_asModule_free, mapDomainAlgHom_apply, mapDomainRingHom_comp_algebraMap, Subrepresentation.subrepresentationSubmoduleOrderIso_apply, Representation.asAlgebraHom_mem_of_forall_mem, domCongr_refl, commRingEquiv_single_single, domCongr_apply, mapDomainBialgHom_id, instIsDomainOfIsCancelAddOfUniqueProds, lift_single, curryAlgEquiv_single, Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule, Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply, lift_of, lift_unique'
|
single 📖 | CompOp | 78 mathmath: mapDomainRingEquiv_single, mapRangeRingHom_single, Representation.asAlgebraHom_single, tensorEquiv.invFun_tmul, antipode_single, mul_def, opRingEquiv_single, single_one_mul_apply, single_eq_zero, lift_symm_apply, mapDomainAddEquiv_single, mapRangeRingEquiv_single, coe_algebraMap, single_mul_apply, Representation.single_smul, mapRangeAlgHom_single, domCongr_single, basis_apply, single_algebraMap_eq_algebraMap_mul_of, liftNCRingHom_single, AddMonoidAlgebra.tensorEquiv.invFun_tmul, singleAddHom_apply, intCast_def, support_mul_single_eq_image, lsingle_apply, single_mul_apply_aux, ofMagma_apply, lift_unique, tensorEquiv_symm_single, opRingEquiv_symm_single, Representation.asAlgebraHom_single_one, ringHom_ext_iff, smul_single, curryRingEquiv_symm_single, commAlgEquiv_single_single, single_mul_single, smul_of, support_mul_single_subset, LinearMap.conjugate_apply, liftNC_single, smul_single', single_commute, single_one_comm, sum_single, singleHom_apply, support_mul_single, mul_single_apply_of_not_exists_mul, mul_single_one_apply, support_single_mul_eq_image, GroupSMul.linearMap_apply, curryRingEquiv_single, scalarTensorEquiv_symm_single, comul_single, support_single_mul, mapDomain_single, single_zero, one_def, single_commute_single, curryAlgEquiv_symm_single, single_add, single_eq_algebraMap_mul_of, mapRangeAddEquiv_single, single_neg, single_pow, singleOneAlgHom_apply, mul_single_apply, single_apply, support_single_mul_subset, single_mul_apply_of_not_exists_mul, counit_single, commRingEquiv_single_single, natCast_def, lift_single, curryAlgEquiv_single, sum_single_index, of_apply, mul_single_apply_aux, prod_single
|
singleAddHom 📖 | CompOp | 3 mathmath: singleAddHom_apply, singleOneRingHom_apply, addHom_ext'_iff
|
singleHom 📖 | CompOp | 1 mathmath: singleHom_apply
|
singleOneRingHom 📖 | CompOp | 5 mathmath: isLocalHom_singleOneRingHom, CommRingCat.monoidAlgebra_map, singleOneRingHom_apply, ringHom_ext'_iff, CommRingCat.monoidAlgebra_obj
|
smulZeroClass 📖 | CompOp | 14 mathmath: smulCommClass, smulCommClass_self, FreeLieAlgebra.liftAux_map_smul, faithfulSMul, smul_single, smul_of, smul_single', smul_apply, smulCommClass_symm_self, FreeLieAlgebra.Rel.smulOfTower, liftNC_smul, isScalarTower_self, isCentralScalar, isScalarTower
|
unexpander 📖 | CompOp | — |
unique 📖 | CompOp | — |
uniqueRingEquiv 📖 | CompOp | 2 mathmath: uniqueRingEquiv_apply, uniqueRingEquiv_symm_apply
|
«term__[_]» 📖 | CompOp | — |