| Name | Category | Theorems |
|---|
instAddCommMonoidWithOne π | CompOp | β |
instAddMonoidWithOne π | CompOp | 138 mathmath: Tactic.NormNum.isInt_lcm, WittVector.RecursionMain.succNthDefiningPoly_degree, Polynomial.degree_pow_le_of_le, Mathlib.Meta.NormNum.IsNNRat.natFloor, Polynomial.coe_lt_degree, ENat.some_eq_coe, Polynomial.MonicDegreeEq.degree, Polynomial.degree_quadratic_lt, Mathlib.Meta.NormNum.isNat_natAbs_pos, MeasureTheory.smul_le_stoppedValue_hittingBtwn, Polynomial.Sequence.degree_eq', PowerSeries.degree_weierstrassMod_lt, Polynomial.degree_eq_natDegree, MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime, Mathlib.Tactic.Ring.coeff_one, WithBot.add_eq_two_iff, cast_withTop, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Lagrange.eq_interpolate_iff, Polynomial.degree_X_pow_add_C, PowerSeries.degree_trunc_lt, Polynomial.card_roots_map_le_degree, Cubic.degree_of_a_eq_zero', MvPolynomial.degree_optionEquivLeft, Polynomial.Splits.degree_eq_card_roots, Cubic.degree_of_a_ne_zero', Polynomial.degree_quadratic, minpoly.degree_le, PowerSeries.IsWeierstrassDivisionAt.degree_lt, Polynomial.degree_cubic_lt, Matrix.charpoly_degree_eq_dim, Mathlib.Meta.NormNum.IsNNRat.natCeil, Polynomial.Chebyshev.degree_T, MeasureTheory.stoppedValue_lowerCrossingTime, instCharZero, Polynomial.degree_X_pow_le, Polynomial.degree_monomial_le, Polynomial.natDegree_lt_iff_degree_lt, Lagrange.degree_interpolate_erase_lt, Polynomial.degree_quadratic_le, Lagrange.degree_interpolate_lt, Polynomial.Sequence.degree_eq, Mathlib.Meta.NormNum.IsNat.natCeil, Polynomial.exists_approx_polynomial_aux, Polynomial.degree_freeMonic, PowerBasis.mem_span_pow', WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, Polynomial.degree_derivative_eq, Polynomial.degree_le_of_natDegree_le, WithBot.add_eq_three_iff, PowerBasis.degree_minpoly, Mathlib.Tactic.Ring.natCast_nat, Polynomial.degree_hermite, Lagrange.degree_nodal, MeasureTheory.StronglyAdapted.isStoppingTime_crossing, Polynomial.degree_X_pow_sub_C, MeasureTheory.stoppedValue_upperCrossingTime, Mathlib.Tactic.Ring.atom_pf', Polynomial.degree_le_natDegree, Mathlib.Meta.NormNum.IsRat.natFloor, Polynomial.exists_multiset_roots, Ideal.mem_leadingCoeffNth, MeasureTheory.smul_le_stoppedValue_hitting, Polynomial.degree_C_mul_X_pow_le, Polynomial.Chebyshev.degree_U_of_ne_neg_one, Polynomial.degreeLT_succ_eq_degreeLE, Polynomial.degree_eq_iff_natDegree_eq_of_pos, Ideal.is_fg_degreeLE, Mathlib.Tactic.Ring.pow_one_cast, Equiv.Perm.toList_formPerm_nontrivial, Polynomial.degree_cubic, Cubic.degree_of_a_eq_zero, Polynomial.degree_X_pow, Cubic.equiv_symm_apply_b, Lagrange.degree_basis, Tactic.NormNum.isInt_gcd, WeierstrassCurve.Affine.degree_polynomial, LinearRecurrence.charPoly_degree_eq_order, MeasureTheory.le_sub_of_le_upcrossingsBefore, Mathlib.Meta.NormNum.IsNat.raw_refl, Lagrange.degree_interpolate_le, Cubic.degree_of_a_ne_zero, MvPolynomial.degree_finSuccEquiv, Field.primitive_element_iff_minpoly_degree_eq, Matrix.charpoly_sub_diagonal_degree_lt, Cubic.equiv_symm_apply_c, Mathlib.Meta.NormNum.IsRat.natCeil, Mathlib.Tactic.Ring.const_pos, Polynomial.card_roots, Polynomial.ofFn_degree_lt, Polynomial.degree_eq_card_roots, PowerBasis.degree_minpolyGen, Polynomial.degree_lt_iff_coeff_zero, cast_withBot, Polynomial.degree_cyclotomic', Polynomial.le_degree_of_ne_zero, Cubic.equiv_apply_coe, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, Polynomial.le_degree_of_mem_supp, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, PowerSeries.isWeierstrassDivisionAt_iff, MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime, Polynomial.degree_update_le, ArithmeticFunction.natCoe_nat, Polynomial.integralNormalization_coeff, Cubic.degree_of_b_ne_zero', Polynomial.degree_shiftedLegendre, Polynomial.span_le_degreeLE_of_finite, Mathlib.Meta.NormNum.IsInt.natCeil, Polynomial.degree_cubic_le, Cubic.equiv_symm_apply_d, Mathlib.Meta.NormNum.IsInt.natFloor, Irreducible.degree_le_two, Tactic.NormNum.isNat_ratDen, Polynomial.degree_eq_card_roots', MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt, Mathlib.Tactic.Ring.atom_pf, Cubic.equiv_symm_apply_a, Mathlib.Meta.NormNum.isNat_natAbs_neg, Mathlib.Tactic.Ring.toProd_pf, Polynomial.degree_sum_fin_lt, Polynomial.degree_eq_iff_natDegree_eq, Polynomial.degreeLE_eq_span_X_pow, Polynomial.natDegree_le_iff_degree_le, Polynomial.degree_monomial, Polynomial.degree_mul_X_pow, WithBot.coe_nonneg, Polynomial.degree_C_mul_X_pow, Polynomial.Chebyshev.degree_U_natCast, Polynomial.degree_cyclotomic, Mathlib.Meta.NormNum.IsNat.natFloor, Polynomial.card_roots_sub_C, Polynomial.mem_degreeLT, PowerBasis.dim_le_degree_of_root, Polynomial.degree_linear_lt, Polynomial.exists_mul_add_mul_eq_C_resultant, Cubic.degree_of_b_ne_zero, Polynomial.roots_def
|
instCommSemiring π | CompOp | 56 mathmath: Polynomial.degree_pow_le_of_le, DivisibleHull.archimedeanClassMk_mk_eq, QuadraticMap.canLift, ComplexShape.eulerCharSignsDownNat_Ο, uzpow_natCast, DivisibleHull.mk_add_mk_left, mem_subalgebraOfSubsemiring, uzpow_coe_nat, ComplexShape.Ξ΅_down_β, Polynomial.degree_comp, ENat.lift_one, NonUnitalSubsemiring.unitization_apply, NNRat.isFractionRing, DivisibleHull.instIsStrictOrderedModuleNNRat, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, subalgebraOfSubsemiring_toSubsemiring, nat_algebra_subsingleton, mem_maximalIdeal_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, DivisibleHull.coeAddMonoidHom_apply, DivisibleHull.instIsOrderedCancelAddMonoid, Subbimodule.coe_toSubbimoduleInt, Polynomial.evalRingHom_zero, DivisibleHull.qsmul_def, Subbimodule.coe_toSubbimoduleNat, QuadraticMap.canLift', DivisibleHull.qsmul_of_nonneg, DivisibleHull.coeOrderAddMonoidHom_apply, DivisibleHull.nsmul_mk, RingHom.toNatAlgHom_coe, Ideal.isPrime_nat_iff, ComplexShape.eulerCharSignsUpNat_Ο, DivisibleHull.mk_add_mk, DivisibleHull.archimedeanClassOrderIso_apply, ringKrullDim_nat, DivisibleHull.zsmul_mk, DivisibleHull.neg_mk, NonUnitalSubsemiring.unitization_range, DivisibleHull.qsmul_of_nonpos, DivisibleHull.archimedeanClassOrderIso_symm_apply, maximalIdeal_eq_span_two_three, MvPolynomial.counitNat_C, DivisibleHull.instIsStrictOrderedModuleRat, DivisibleHull.coe_add, mem_nonUnitalSubalgebraOfNonUnitalSubsemiring, RingHom.toNatAlgHom_apply, DivisibleHull.mk_zero, DivisibleHull.zero_qsmul, MvPolynomial.counitNat_X, fermatLastTheoremWith'_nat_int_tfae, MvPolynomial.counitNat_surjective, isCoprime_iff, PNat.isCoprime_iff, coe_maximalIdeal, DivisibleHull.nnqsmul_mk, Algebra.adjoin_nat
|
instDistrib π | CompOp | β |
instNonAssocSemiring π | CompOp | 19 mathmath: addMonoidHomLequivNat_symm_apply, AddMonoidHom.toNatLinearMap_injective, AddEquiv.toNatLinearEquiv_toAddEquiv, AddEquiv.toNatLinearEquiv_trans, castRingHom_nat, AddMonoidHom.coe_toNatLinearMap, AddCommGroup.DirectLimit.directedSystem, RingHom.injective_nat, coe_castRingHom, AddEquiv.coe_symm_toNatLinearEquiv, addMonoidHomLequivNat_apply, Ideal.map_comap_natCastRingHom_int, AddEquiv.coe_toNatLinearEquiv, LinearEquiv.toAddEquiv_toNatLinearEquiv, AddEquiv.toNatLinearEquiv_symm, CharP.quotient_iff_le_ker_natCast, MonoidWithZeroHom.ext_int_iff, MonoidWithZeroHomClass.ext_nnrat_iff, MonoidHom.ext_int_iff
|
instNonUnitalNonAssocSemiring π | CompOp | 10 mathmath: floorDiv_eq_div, isLinearSet_iff_exists_matrix, instTrivialStar, ceilRoot_def, factorization_ceilRoot, isSemilinearSet_setOf_mulVec_eq, factorization_floorRoot, floorRoot_def, StarAddMonoid.toStarModuleNat, ceilDiv_eq_add_pred_div
|
instNonUnitalSemiring π | CompOp | 2 mathmath: instStarOrderedRing, isQuasiregular_zero
|
instSemiring π | CompOp | 232 mathmath: odd_fermatNumber, Submodule.toAddSubmonoid_toNatSubmodule, pow_eq_neg_pow_iff, iSupIndep.dfinsupp_lsum_injective, Submodule.span_nat_eq_addSubmonoid_closure, Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, MvPowerSeries.weightedOrder_monomial, addMonoidHomLequivNat_symm_apply, MvPolynomial.weightedDegree_eq_zero_iff, ofDigits_lt_base_pow_length, PowerSeries.catalanSeries_coeff, PowerSeries.coeff_X_mul_largeSchroderSeries, neg_one_pow_eq_neg_one_iff_odd, AddCommMonoid.subsingletonNatModule, four_dvd_or_exists_odd_prime_and_dvd_of_two_lt, OreLocalization.nsmul_eq_nsmul, Finsupp.le_weight_of_ne_zero', ofDigits_one, Fintype.linearIndependent_iff', Odd.natAbs, Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff, sum_le_ofDigits, odd_add_one, exists_mem_span_nat_finset_of_ge, PowerSeries.catalanSeries_constantCoeff, Finset.even_sum_iff_even_card_odd, odd_totient_iff, MvPolynomial.le_weightedTotalDegree, ZMod.natCast_eq_one_iff_odd, Set.odd_ncard_compl_iff, ofDigits_lt_base_pow_length', odd_sub', Submodule.biSup_eq_range_dfinsupp_lsum, AddMonoidHom.toNatLinearMap_injective, ZMod.isCyclic_units_iff, ofDigits_eq_sum_mapIdx, ascPochhammer_nat_eq_descFactorial, ofDigits_append_zero, infinite_odd_deficient, geom_sum_pos_iff, Set.odd_card_insert_iff, AddEquiv.toNatLinearEquiv_toAddEquiv, MvPowerSeries.weightedOrder_monomial_of_ne_zero, ZMod.natCast_ne_zero_iff_odd, infinite_odd_abundant, ofDigits_digits_append_digits, Equiv.Perm.sign_of_cycleType_eq_replicate, odd_totient_iff_eq_one, ofDigits_mod_pow_eq_ofDigits_take, pow_length_le_mul_ofDigits, subset_span_setGcd, Submodule.span_nat_eq, PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq, AddSubmonoid.toNatSubmodule_toAddSubmonoid, MvPowerSeries.X_def, AddSubmonoid.toNatSubmodule_closure, AlternatingGroup.card_of_cycleType_singleton, NonUnitalSubsemiring.unitization_apply, ComplexShape.down_nat_odd_add, Polynomial.smeval_neg_nat, bijOn_ofDigits, DFinsupp.sum_mapRange_index.linearMap, injOn_ofDigits, Int.odd_coe_nat, PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, finite_setOf_setGcd_dvd_and_mem_span, ofDigits_mod_eq_head!, ArithmeticFunction.zeta_mul_pow_eq_sigma, Submodule.mem_iSup_iff_exists_dfinsupp, not_odd_iff_even, Submodule.iSup_eq_range_dfinsupp_lsum, CategoryTheory.Functor.natLinear, ofDigits_div_pow_eq_ofDigits_drop, bijOn_ofDigits', ArithmeticFunction.zeta_mul_comm, SimpleGraph.even_card_odd_degree_vertices, Finsupp.finite_of_nat_weight_le, Finsupp.le_weight, Prime.odd_of_ne_two, Module.isTorsionFree_nat_iff_isAddTorsionFree, Set.even_card_insert_iff, instIsDomain, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, ofDigits_monotone, not_even_iff_odd, Fin.odd_iff_of_even, frequently_odd, ofDigits_replicate_zero, PowerSeries.coeff_largeSchroderSeries, Fintype.linearIndependent_iff'β, AddEquiv.toNatLinearEquiv_trans, AddMonoidHom.coe_toNatLinearMap, MvPowerSeries.le_weightedOrder_subst, isProperLinearSet_iff, ofDigits_cons, coprime_two_left, coprime_two_right, Polynomial.smeval_at_natCast, AddMonoid.FG.to_moduleFinite_nat, MvPowerSeries.coeff_weightedHomogeneousComponent, Ring.ascPochhammer_succ_succ, Fin.even_iff, sum_digits_ofDigits_eq_sum, instIsLocalRingNat, AddSubmonoid.toNatSubmodule_symm, floor_nat, Equiv.Perm.centralizer_le_alternating_iff, BinomialRing.factorial_nsmul_multichoose, odd_pow_iff, Module.End.natCast_def, ceil_nat, MonoidHom.FixedPointFree.odd_orderOf_of_involutive, orderedSMul, Finset.odd_sum_iff_odd_card_odd, AddMonoid.End.natCast_def, ofDigits_nil, ascPochhammer_nat_eval_succ, fermatLastTheoremWith_nat_int_rat_tfae, Ring.smeval_ascPochhammer_int_ofNat, odd_mul, PowerSeries.constantCoeff_largeSchroderSeries, fermatLastTheoremFor_iff_nat, ofDigits_reverse_cons, coe_ofDigits, even_sub', Fin.odd_iff_imp, Ring.smeval_ascPochhammer_nat_cast, Submodule.fg_iff_addSubmonoid_fg, AddCommGroup.DirectLimit.directedSystem, ComplexShape.up_nat_odd_add, Polynomial.sumIDeriv_X, Polynomial.ascPochhammer_smeval_cast, MvPowerSeries.weightedOrder_eq_nat, instIsNoetherian, LieModule.chainTopCoeff_add_one, ofDigits_mod, Fin.even_succAbove_add_predAbove, setInvOn_digitsAppend_ofDigits, even_xor_odd, MvPowerSeries.map_iterateFrobenius_expand, Ideal.isPrime_nat_iff, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, Submodule.span_nat_eq_addSubmonoidClosure, nat_smul_eq_nsmul, MvPowerSeries.weightedOrder_le, AddEquiv.toNatLinearEquiv_refl, Matrix.toLinearMapβ'_single, Fin.odd_iff, Prime.eq_two_or_odd', Int.natAbs_odd, MvPolynomial.weightedDecomposition.decompose'_eq, not_odd_iff, Finsupp.le_weight_of_ne_zero, Ring.smeval_ascPochhammer_neg_add, Module.Basis.toMatrix_eq_toMatrix_constr, even_add', ofDigits_append, odd_add', AddEquiv.coe_symm_toNatLinearEquiv, addMonoidHomLequivNat_apply, ArithmeticFunction.mul_zeta_apply, Function.Involutive.iterate_eq_self, AddMonoid.isTorsion_iff_isTorsion_nat, iSupIndep_iff_dfinsupp_lsum_injective, sub_one_mul_sum_div_pow_eq_sub_sum_digits, SimpleGraph.odd_ncard_oddComponents, Ring.smeval_ascPochhammer_succ_neg, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, NonUnitalSubsemiring.unitization_range, AddSubmonoid.coe_toNatSubmodule, PowerSeries.catalanSeries_sq_mul_X_add_one, Polynomial.ascPochhammer_smeval_eq_eval, Ideal.map_comap_natCastRingHom_int, Finsupp.weight_sub_single_add, digits_ofDigits, ascPochhammer_eval_cast, ofDigits_singleton, instIsStrictOrderedRing, AddEquiv.coe_toNatLinearEquiv, ofDigits_reverse_zero_cons, MonoidHom.FixedPointFree.odd_card_of_involutive, Ring.smeval_ascPochhammer_neg_of_lt, Module.Finite.iff_addMonoid_fg, mersenne_odd, Cubic.monic_of_d_eq_one', DistribSMul.toAddMonoidHom_eq_nsmulAddMonoidHom, ofDigits_append_replicate_zero, pow_eq_neg_one_iff, eq_two_pow_or_exists_odd_prime_and_dvd, odd_sub, ascPochhammer_nat_eq_ascFactorial, schnirelmannDensity_setOf_Odd, Coprime.odd_of_left, LinearEquiv.toAddEquiv_toNatLinearEquiv, SimpleGraph.Coloring.odd_length_iff_not_congr, self_mod_pow_eq_ofDigits_take, isCompl_even_odd, AddEquiv.toNatLinearEquiv_symm, MvPolynomial.coeff_weightedHomogeneousComponent, ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq, ofDigits_modEq, ArithmeticFunction.natCoe_mul, CharP.quotient_iff_le_ker_natCast, exists_eq_two_pow_mul_odd, Submodule.mem_biSup_iff_exists_dfinsupp, Coprime.odd_of_right, ArithmeticFunction.zeta_mul_apply, Polynomial.descPochhammer_smeval_eq_ascPochhammer, ofDigits_modEq', mul_ofDigits, even_or_odd, ZMod.ne_zero_iff_odd, Ring.smeval_ascPochhammer_self_neg, SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp, CoxeterSystem.IsReflection.odd_length, one_mem_span_iff, Finsupp.weight_eq_zero_iff_eq_zero, odd_iff, SimpleGraph.Walk.IsEulerian.card_odd_degree, ofDigits_div_eq_ofDigits_tail, MvPolynomial.weightedHomogeneousComponent_apply, self_div_pow_eq_ofDigits_drop, lsum_comp_mapRange_toSpanSingleton, mapsTo_ofDigits, IsAddTorsionFree.to_isTorsionFree_nat, Odd.mod_even_iff, not_odd_zero, odd_add, Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup, ofDigits_digits, ZMod.eq_one_iff_odd
|