card 📖 | CompOp | 755 mathmath: card_pi, all_card_le_rel_image_card_iff_exists_injective, PiLp.lipschitzWith_toLp, PiLp.norm_toLp_const', Matrix.GeneralLinearGroup.det_scalar, card_le_of_injective, AddChar.card_addChar_le, pow_card_eq_one, card_congr, Algebra.norm_algebraMap_of_basis, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, Set.card_fintypeInsertOfNotMem, Function.minimalPeriod_le_card, FixedPoints.finrank_eq_card, LucasLehmer.X.card_eq, Finset.card_univ, card_coeSort_range, TruncatedWittVector.card, tendsto_tsum_div_pow_atTop_integral, linearIndependent_iff_card_le_finrank_span, addOrderOf_eq_card_multiples, card_ofFinset, modularCyclotomicCharacter.id, linearIndependent_le_span, quadraticChar_card_card, ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, Finset.dens_cons, card_coeSort_mrange, one_lt_card, card_subtype_le, Int.card_fintype_addEquiv, IsLowerSet.le_card_inter_finset, Polynomial.card_rootSet_le_derivative, Matrix.coeff_charpoly_mem_ideal_pow, Finset.sum_card_le, List.Nodup.length_le_card, Sym2.card_subtype_not_diag, Matrix.rank_add_rank_le_card_of_mul_eq_zero, MeasureTheory.integral_fintype_prod_volume_eq_pow, FiniteField.pow_card_sub_one_eq_one, PiLp.norm_toLp_one, Module.Basis.card_le_card_of_linearIndependent, card_fin_two, SzemerediRegularity.a_add_one_le_four_pow_parts_card, Equiv.Perm.card_of_cycleType_mul_eq, SimpleGraph.degree_lt_card_verts, card_fin, Finset.doubling_lt_three_halves, sum_hom_units, Finset.card_compl_add_card, linearIndependent_le_span', Finset.card_mul_dens, Monovary.sum_mul_sum_le_card_mul_sum, SimpleGraph.minDegree_lt_card, card_range_le, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, mod_card_zsmul, SimpleGraph.isExtremal_top_free_iff_isTuranMaximal, set_fintype_card_eq_univ_iff, AddChar.sum_mulShift, cyclotomicCharacter.toZModPow, FiniteField.frobeniusAlgEquivOfAlgebraic_apply, expect_dite_eq, LieAlgebra.rank_le_card, DihedralGroup.card, QuotientGroup.card_quotient_rightRel, FiniteField.frobeniusAlgHom_apply, rank_eq_card_basis, card_perm, SimpleGraph.extremalNumber_le_iff_of_nonneg, Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose, NumberField.InfinitePlace.card_mono, Finset.local_lubell_yamamoto_meshalkin_inequality_mul, Finset.card_eq_iff_eq_univ, Finset.mulEnergy_univ_left, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, Finset.mulEnergy_univ_right, quadraticChar_two, FiniteField.isPrimePow_card, Matrix.det_le, Set.Intersecting.is_max_iff_card_eq, LinearIndependent.rank_matrix, SimpleGraph.IsClique.card_le_of_coloring, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, Equiv.Perm.OnCycleFactors.kerParam_range_card, IsCyclic.unique_zpow_zmod, Finset.card_mul_le_card_shadow_mul, card_Iic, Finset.card_add_card_compl, IsAddCyclic.unique_zsmul_zmod, expect_ite_eq, card_equiv, Matrix.rank_one, Real.volume_pi_ball, SimpleGraph.card_set_walk_length_eq, card_subtype_or, jacobiSum_trivial_trivial, SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, Matrix.trace_eq_neg_charpoly_coeff, FixedPoints.rank_le_card, SimpleGraph.card_edgeFinset_le_card_choose_two, Matrix.charpoly_natCast, Complex.volume_sum_rpow_le, CategoryTheory.FinCategory.categoryAsType_comp, card_subtype_mono, AddMonoidAlgebra.cardinalMk_lift_of_fintype, AddChar.sum_eq_ite, finrank_algHom, Function.Embedding.nonempty_iff_card_le, expect_ite_zero, CategoryTheory.FinCategory.asTypeToObjAsType_map, MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero, SimpleGraph.farFromTriangleFree_iff, QuadraticMap.discr_smul, LinearMap.rank_diagonal, Matrix.rank_of_isUnit, FiniteField.coe_frobeniusAlgEquivOfAlgebraic, SimpleGraph.card_incidenceSet_eq_degree, IsLowerSet.card_inter_le_finset, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, MeasureTheory.integral_fintype_prod_eq_pow, SzemerediRegularity.m_le_card_of_mem_chunk_parts, FiniteField.card_algEquiv_extension, BoxIntegral.Prepartition.card_filter_mem_Icc_le, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, Matrix.det_updateRow_smul_left, SimpleGraph.card_commonNeighbors_le_degree_left, AffineIndependent.finrank_vectorSpan_add_one, Pi.sum_norm_apply_le_norm', BoxIntegral.unitPartition.integralSum_eq_tsum_div, expect_dite_eq', FiniteField.cast_card_eq_zero, card_range, Finset.card_div_choose_le_card_shadow_div_choose, sum_piFinset_apply, QuaternionGroup.card, Algebra.Norm.Transitivity.comp_det_mul_pow, Matrix.det_smul, modularCyclotomicCharacter.toFun_spec', SimpleGraph.IsSRGWith.card_neighborFinset_union_eq, card_of_isEmpty, tendsto_card_div_pow_atTop_volume, SimpleGraph.chromaticNumber_top, orderOf_le_card_univ, Nat.count_eq_card_fintype, Finset.sum_card, FiniteField.pow_card_pow, Finset.card_compl, Finset.local_lubell_yamamoto_meshalkin_inequality_div, AddChar.sum_apply_eq_ite, addOrderOf_le_card_univ, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, Equiv.Perm.sign_of_cycleType_eq_replicate, AffineIndependent.card_le_finrank_succ, Matrix.det_kroneckerMapBilinear, IsAddKleinFour.card_four', SimpleGraph.Walk.IsHamiltonianCycle.length_eq, SimpleGraph.Partition.colorable, Matrix.frobenius_nnnorm_one, MvPolynomial.rank_R, SimpleGraph.card_neighborSet_eq_degree, Equiv.Perm.VectorsProdEqOne.card, PiLp.nnnorm_toLp_one, Matrix.cRank_le_card_height, FiniteField.roots_X_pow_card_sub_X, SimpleGraph.IsRegularOfDegree.compl, card_set, SimpleGraph.Subgraph.IsPerfectMatching.even_card, Finset.addEnergy_univ_left, SimpleGraph.ConnectedComponent.even_card_of_isPerfectMatching, ZLattice.covolume.tendsto_card_div_pow, Equiv.Perm.sumCongrHom.card_range, card_le_of_injective, SimpleGraph.card_edgeFinset_of_isExtremal_free, AddChar.sum_eq_card_of_eq_one, ContinuousMultilinearMap.norm_image_sub_le, SimpleGraph.Adj.card_commonNeighbors_lt_degree, card_units, Nat.card_units_zmod_lt_sub_one, Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose, SimpleGraph.IsSRGWith.top, MulChar.orderOf_dvd_card_sub_one, MulAction.card_eq_sum_card_group_div_card_stabilizer, Matrix.card_GL_field, card_subtype_lt, SimpleGraph.IsSRGWith.card, SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty, two_lt_card_iff, Polynomial.card_rootSet_eq_natDegree_iff_of_splits, Subring.card_top, SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraph, FiniteField.odd_card_of_char_ne_two, Matrix.det_smul_of_tower, Equiv.Perm.fixed_point_card_lt_of_ne_one, CategoryTheory.FinCategory.categoryAsType_id, Sym.card_sym_eq_choose, Set.coe_fintypeCard, card_setUniv, card_pi_const, card_pempty, SimpleGraph.card_edgeFinset_le_extremalNumber, SimpleGraph.farFromTriangleFree.le_card_sub_card, Equiv.Perm.card_of_cycleType_eq_zero_iff, FiniteField.forall_pow_eq_one_iff, composition_card, Matrix.charpoly_zero, Finset.biUnion_slice, card_embedding_eq_of_unique, card_units_lt, card_eq_one_iff_nonempty_unique, Cardinal.mk_toNat_eq_card, MeasureTheory.volume_sum_rpow_lt, Matrix.charpoly_degree_eq_dim, Real.dimH_ball_pi, SimpleGraph.isExtremal_free_iff, prime_dvd_char_iff_dvd_card, Finset.card_lt_iff_ne_univ, MulChar.pow_card_eq_one, FixedPoints.finrank_le_card, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, card_Ici, card_nsmul_eq_zero, AlgEquiv.card_le, Matrix.adjugate_adjugate, IsPrimitiveRoot.card_rootsOfUnity', PiLp.nnnorm_toLp_const', MeasureTheory.hausdorffMeasure_pi_real, Int.card_fintype_Ioo_of_lt, card_le_one_iff, FiniteField.card_image_polynomial_eval, AhlswedeZhang.IsAntichain.le_infSum, card_mul_expect, Matrix.det_sum_le, card_Icc, Finset.le_sum_card, hammingNorm_le_card_fintype, Equiv.Perm.card_fixedPoints_modEq, Configuration.ProjectivePlane.card_points, SimpleGraph.chromaticNumber_le_card, card_Ioo, subtype_card, IsAntichain.sperner, card_additive, ZMod.card_units, ZMod.card_units_eq_totient, MulAction.card_eq_sum_card_group_div_card_stabilizer', Submonoid.card_bot, Matrix.cRank_le_card_width, sum_conjClasses_card_eq_card, FDRep.average_char_eq_finrank_invariants, modularCyclotomicCharacter.toFun_spec, Nat.cast_card_eq_zero, card_sigma, Equiv.Perm.card_isConj_eq, addOrderOf_dvd_card, card_vector, IsPrimitiveRoot.card_rootsOfUnity, MeasureTheory.volume_sum_rpow_le, MultilinearMap.map_update_smul_left, card_eq, CategoryTheory.FinCategory.asTypeToObjAsType_obj, Finset.dens_eq_card_div_card, MulChar.sum_one_eq_card_units, card_fin_lt_of_le, Finset.sum_card_slice, MvPolynomial.map_restrict_dom_evalₗ, ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall, iSupIndep.subtype_ne_bot_le_finrank, Matrix.det_kronecker, Char.card_pow_card, SimpleGraph.chromaticNumber_eq_card_iff, MultilinearMap.domCoprod_alternization_eq, Equiv.Perm.subtypeCongrHom.card_range, PMF.uniformOfFintype_apply, Finset.card_eq_of_equiv_fintype, PNat.card_fintype_uIcc, card_eq_of_linearEquiv, card_of_bijective, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, coe_smulCardAddSubgroup, LucasLehmer.X.card_units_lt, IsUpperSet.le_card_inter_finset, SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts, MvPolynomial.finrank_R, SimpleGraph.extremalNumber_top, Polynomial.coeff_det_X_add_C_card, card_classGroup_eq_one_iff, Equiv.Perm.card_of_cycleType, ConjAct.card, SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber, NumberField.Embeddings.card, card_of_finset', Module.card_eq_pow_finrank, card_eq_zero, orderOf_dvd_card, Module.finrank_pi, AddMonoidAlgebra.cardinalMk_of_fintype, Matrix.IsHermitian.eigenvalues₀_antitone, SimpleGraph.card_commonNeighbors_le_degree_right, finrank_euclideanSpace, SimpleGraph.adjMatrix_pow_apply_eq_card_walk, card_subtype_true, CategoryTheory.FinCategory.objAsTypeToAsType_map, card_subtype_or_disjoint, Finset.doubling_lt_two, Set.card_ne_eq, Int.card_fintype_Icc_of_le, addRothNumber_le_ruzsaSzemerediNumber, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, finrank_range_le_card, ruzsaSzemerediNumber_le, SimpleGraph.dart_card_eq_twice_card_edges, Matrix.charpoly_one, SimpleGraph.isExtremal_top_free_turanGraph, Finset.dens_mul_card, Finset.expect_boole_mul', NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace, Equiv.Perm.sign_of_pow_two_eq_one, AddAction.minimalPeriod_eq_card, Set.Finite.card_toFinset, isPrimePow_card_of_field, bijective_iff_surjective_and_card, FiniteField.two_pow_card, MvPolynomial.indicator_mem_restrictDegree, SimpleGraph.card_neighborSet_toSubgraph, quadraticChar_neg_two, AddChar.card_eq, Module.finrank_eq_card_basis, Set.toFinset_card, Set.card_range_of_injective, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate, MvPolynomial.psum_zero, AlternatingMap.norm_image_sub_le_of_bound, Pi.sum_nnnorm_apply_le_nnnorm, Pi.sum_norm_apply_le_norm, bijective_iff_injective_and_card, Algebra.Norm.Transitivity.det_det_aux, MvPolynomial.degrees_indicator, PMF.toMeasure_uniformOfFintype_apply, card_derangements_fin_add_two, Int.card_fintype_Ioc_of_le, card_subtype, finrank_span_eq_card, card_prod, Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀, Equiv.Perm.card_compl_support_modEq, card_finset, AlternatingGroup.card_of_cycleType, Equiv.Perm.sum_cycleType_le, card_option, pow_gcd_card_eq_one_iff, AlgHom.card_of_powerBasis, Cardinal.mk_fintype, AddSubmonoid.eq_bot_iff_card, Ideal.rank_eq, Matrix.adjugate_smul, SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq, Set.Sized.compls, one_lt_card_iff_nontrivial, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, nonempty_field_iff, SimpleGraph.IsContained.bot, AddGroup.exponent_dvd_card, Complex.volume_sum_rpow_lt, Equiv.Perm.centralizer_le_alternating_iff, card_filter_piFinset_const_eq_of_mem, Pi.sum_nnnorm_apply_le_nnnorm', Matrix.square_of_invertible, Polynomial.cardPowDegree_apply, ofEquiv_card, SimpleGraph.bot_isContained_iff_card_le, FiniteField.unit_isSquare_iff, Module.finrank_matrix, Matrix.adjugate_adjugate', card_lt_of_surjective_not_injective, Submodule.IsLattice.finrank_of_pi, Equiv.Perm.card_fixedPoints, Set.card_lt_card, Matrix.rank_le_card_width, Submonoid.card_le_one_iff_eq_bot, Function.mem_periodicPts_iff_isPeriodicPt_factorial_card, FiniteField.Matrix.charpoly_pow_card, Submodule.IsLattice.rank_of_pi, FiniteField.trace_pow_card, Set.card_image_of_injective, Sym2.card_diagSet_compl, PiLp.antilipschitzWith_ofLp, Cardinal.mk_finsupp_of_fintype, card_punit, Finset.sum_card_slice_div_choose_le_one, SimpleGraph.Subgraph.IsSpanning.card_verts, AffineSubspace.card_pos_of_affineSpan_eq_top, DomMulAct.stabilizer_card', AhlswedeZhang.infSum_compls_add_supSum, Module.Basis.card_le_card_of_submodule, card_eq_sum_ones, Matrix.det_adjugate, Nat.card_eq, Ordinal.type_fintype, MultilinearMap.norm_image_sub_le_of_bound, SimpleGraph.card_commonNeighbors_lt_card_verts, FiniteField.card, ClassGroup.norm_lt, card_ofIsEmpty, ContinuousAlternatingMap.le_opNorm_mul_pow_card_of_le, exists_signed_sum', Set.card_empty, Finset.expect_boole_mul, SimpleGraph.card_support_deleteIncidenceSet, Function.injective_iff_iterate_factorial_card_eq_id, card_lt_of_injective_of_notMem, stdSimplex.barycenter_apply, Polynomial.card_rootSet_eq_natDegree, Function.isPeriodicPt_factorial_card_of_mem_periodicPts, AlternatingMap.coe_alternatization, Module.finrank_eq_card_chooseBasisIndex, Finset.card_lt_univ_of_notMem, Algebra.trace_algebraMap_of_basis, ContinuousMultilinearMap.norm_iteratedFDeriv_le, orderOf_eq_card_powers, Real.dimH_univ_pi, NumberField.InfinitePlace.card_real_embeddings, card_shrink, Finset.nnratCast_dens, PNat.card_fintype_Ioo, ContinuousMultilinearMap.norm_iteratedFDeriv_le', Cardinal.mk_finset_of_fintype, Matrix.det_neg, SimpleGraph.IsSRGWith.of_adj, FiniteField.even_card_of_char_two, two_mul_card_alternatingGroup, ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le, AlgHom.card, ruzsaSzemerediNumberNat_card, card_le_of_injective', compositionAsSet_card, instNeZeroNatCardOfNonempty, AhlswedeZhang.supSum_of_univ_notMem, Matrix.rank_diagonal, Configuration.HasPoints.card_le, SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_adj_compl, LTSeries.length_lt_card, Finset.card_le_univ, Equiv.Perm.sigmaCongrRightHom.card_range, Nat.prime_iff_card_units, Finset.card_biUnion_le_of_intersecting, MonoidAlgebra.cardinalMk_lift_of_fintype, Cardinal.mk_finsupp_lift_of_fintype, SimpleGraph.complete_graph_degree, SzemerediRegularity.card_eq_of_mem_parts_chunk, SimpleGraph.dart_card_eq_sum_degrees, Matrix.charpoly_natDegree_eq_dim, FiniteField.pow_card, PiLp.norm_toLp_const, card_le_card_of_rightTotal_unique, BoxIntegral.TaggedPrepartition.IsHenstock.card_filter_tag_eq_le, FiniteField.pow_dichotomy, SimpleGraph.isNClique_map_copy_top, gaussSum_mul_gaussSum_pow_orderOf_sub_one, AlgHom.card_le, FiniteField.splits_X_pow_card_sub_X, MulAction.mem_fixedPoints_iff_card_orbit_eq_one, Matrix.det_smul_adjugate_adjugate, Cardinal.mk_eq_nat_iff_fintype, card_alternatingGroup, AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one, card_eq_zero_iff, AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup, Matrix.charpoly_sub_diagonal_degree_lt, LinearIndependent.fintype_card_le_finrank, ENat.card_eq_coe_fintype_card, FintypeCat.Skeleton.incl_mk_nat_card, FiniteField.pow_finrank_eq_card, card_plift, set_fintype_card_le_univ, Set.card_le_card, AffineBasis.card_eq_finrank_add_one, EuclideanSpace.volume_ball, FiniteField.isSquare_iff, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, Sym.card_sym_fin_eq_multichoose, card_units_int, card_subtype_eq_or_eq_of_ne, MvPolynomial.prod_C_add_X_eq_sum_esymm, Finset.dens_singleton, TruncatedWittVector.card_zmod, Matrix.charpoly_vecMulVec, quadraticCharFun_eq_pow_of_char_ne_two, GaussianFourier.integral_cexp_neg_mul_sum_add, card_empty, SimpleGraph.completeMultipartiteGraph.chromaticNumber, SimpleGraph.extremalNumber_le_iff, card_unique, VectorSpace.card_fintype, SimpleGraph.Coloring.card_colorClasses_le, ProbabilityTheory.uniformOn_univ, Finset.card_compl_lt_iff_nonempty, SimpleGraph.degree_compl, OrthonormalBasis.norm_le_card_mul_iSup_norm_inner, SimpleGraph.lt_extremalNumber_iff, commProb_function, finrank_le_of_span_eq_top, Real.volume_pi_le_diam_pow, quadraticChar_odd_prime, PNat.card_fintype_Ioc, SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph, Matrix.charpoly.univ_natDegree, FiniteField.sum_pow_units, cyclotomicCharacter.toZModPow_toFun, SimpleGraph.Walk.IsHamiltonian.length_eq, Finset.natCast_card_mul_nnratCast_dens, PNat.card_fintype_Ico, Finset.expect_univ, Polynomial.natDegree_det_X_add_C_le, Fin.card_range_le, Matrix.trace_one, card_quotient_le, card_zpowers_le, SimpleGraph.Walk.isHamiltonianCycle_iff_isCycle_and_length_eq, AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup, CategoryTheory.FinCategory.objAsTypeToAsType_obj, Matrix.rank_le_card_height, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀, card_uIcc, card_eq_one_of_forall_eq, SimpleGraph.IsTuranMaximal.card_parts, Finset.card_mul_finset_lt_two, gaussSum_pow_eq_prod_jacobiSum, modularCyclotomicCharacter.comp, card_zmultiples, SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset, AhlswedeZhang.supSum_singleton, SzemerediRegularity.pow_mul_m_le_card_part, Polynomial.cardPowDegree_nonzero, card_Ioc, FiniteField.frobeniusAlgEquiv_apply, Matrix.charpoly_inv, IsUnramifiedAtInfinitePlaces.card_infinitePlace, ModularForm.prod_fintype_slash, SimpleGraph.card_commonNeighbors_top, IsSimpleOrder.card, Equiv.Perm.card_le_of_centralizer_le_alternating, card_ulift, SimpleGraph.completeBipartiteGraph_isContained_iff, Equiv.Perm.filter_parts_partition_eq_cycleType, card_derangements_eq_numDerangements, card_finsupp, card_derangements_fin_eq_numDerangements, SimpleGraph.lt_extremalNumber_iff_of_nonneg, card_eq_card_units_add_one, card_Ioi, FDRep.char_orthonormal, LinearMap.nilRank_le_card, card_Iio, Setoid.card_classes_ker_le, Antivary.card_mul_sum_le_sum_mul_sum, SzemerediRegularity.coe_m_add_one_pos, SimpleGraph.regularityReduced_edges_card_aux, card_orderDual, Finset.card_shatterer_le_sum_vcDim, SzemerediRegularity.card_aux₂, Module.finrank_finsupp_self, jacobiSum_mul_jacobiSum_inv, Antivary.card_smul_sum_le_sum_smul_sum, Module.card_fintype, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, Complex.card_rootsOfUnity, Matrix.det_neg_eq_smul, SimpleGraph.not_cliqueFree_card_of_top_embedding, SimpleGraph.completeMultipartiteGraph.colorable, NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces, Equiv.Perm.exists_with_cycleType_iff, Configuration.ProjectivePlane.card_lines, Matrix.det_sum_smul_le, FiniteField.expand_card, FiniteField.card', Matrix.det_kroneckerTMul, Matrix.charpoly_mul_comm', card_filter_piFinset_const, quadraticChar_eq_pow_of_char_ne_two, Equiv.Perm.parts_partition, card_unit, card_ofSubsingleton, Matrix.cramer_smul, modularCyclotomicCharacter'.spec', Basis.le_span'', card_embedding_eq_of_infinite, basis_le_span', Int.card_fintype_Ico_of_le, quadraticChar_eq_pow_of_char_ne_two', Sym2.card_subtype_diag, Configuration.HasLines.card_le, card_le_of_surjective, pow_mod_card, tendsto_card_div_pow_atTop_volume', FiniteField.isSplittingField_sub, MonoidAlgebra.cardinalMk_of_fintype, card_finset_len, card_le_of_embedding, card_lex, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer, SimpleGraph.Iso.card_eq, DyckWord.card_dyckWord_semilength_eq_catalan, expect_ite_eq', Numbering.card_prefixed, BoxIntegral.unitPartition.volume_box, Complex.volume_sum_rpow_lt_one, AddSubmonoid.card_le_one_iff_eq_bot, Module.finrank_fintype_fun_eq_card, rank_fun, Equiv.Perm.CycleType.count_def, quadraticChar_neg_one, card_Ico, Matrix.IsHermitian.rank_eq_card_non_zero_eigs, Module.Basis.opNNNorm_le, card_of_subtype, card_le_of_surjective', finrank_vectorSpan_range_add_one_le, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer', rank_fun', sum_pow_mul_eq_add_pow, card_rootsOfUnity, MeasureTheory.GridLines.T_univ, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, coe_powCardSubgroup, card_smul_expect, Configuration.ProjectivePlane.card_points_eq_card_lines, Group.exponent_dvd_card, SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card, rank_fun_eq_lift_mul, Module.Basis.opNorm_le, SimpleGraph.CliqueFree.card_edgeFinset_le, SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul, SimpleGraph.card_edgeSet, Sym2.card, AddSubmonoid.card_bot, exists_signed_sum, AddAction.mem_fixedPoints_iff_card_orbit_eq_one, ContinuousAlternatingMap.norm_compContinuousLinearMap_le, SimpleGraph.card_neighborSet_union_compl_neighborSet, card_compl_set, FiniteField.even_card_iff_char_two, Sym.card_sym_eq_multichoose, one_lt_card_iff, ClassGroup.norm_le, card_multiplicative, card_subtype_eq', card_zpowers, AlgHom.card_of_splits, Numbering.dens_prefixed, IsUpperSet.card_inter_le_finset, Set.card_singleton, Matrix.det_updateCol_smul_left, SimpleGraph.Walk.IsPath.length_lt, card_le_card_of_leftTotal_unique, PiLp.nnnorm_toLp_const, card_subtype_compl, SimpleGraph.IsRegularOfDegree.top, FiniteField.coe_frobeniusAlgHom, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, FDRep.scalar_product_char_eq_finrank_equivariant, Matrix.rank_unit, Module.Basis.card_le_card_of_le, Group.card_center_add_sum_card_noncenter_eq_card, ZLattice.covolume.tendsto_card_div_pow'', card_coe, ConjClasses.card_carrier, mod_card_nsmul, SimpleGraph.IsSRGWith.card_commonNeighbors_eq_of_not_adj_compl, SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, Real.volume_pi_closedBall, LieModule.rank_le_card, PMF.toOuterMeasure_uniformOfFintype_apply, card_classGroup_eq_one, linearIndependent_le_span_aux', Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite, gaussSum_mul_gaussSum_eq_card, card_numbering, NumberField.InfinitePlace.card_complex_embeddings, DomMulAct.stabilizer_card, Matrix.charpoly_ofNat, card_fun, card_pos_iff, PNat.card_fintype_Icc, card_congr', QuotientAddGroup.card_quotient_rightRel, MulAction.minimalPeriod_eq_card, Set.card_image_of_inj_on, SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ, Finset.nnratCast_dens_mul_natCast_card, FiniteField.card_algHom_of_finrank_dvd, card_eq_one_iff, Finset.card_univ_diff, Multiset.card_coe, Matrix.charpoly.univ_coeff_card, SimpleGraph.cliqueFree_iff_top_free, MulChar.apply_mem_rootsOfUnity, Finset.addEnergy_univ_right, card_prop, card_pos, Module.Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff, SimpleGraph.Walk.IsEulerian.card_odd_degree, Matrix.det_eq_sign_charpoly_coeff, Monovary.sum_smul_sum_le_card_smul_sum, EuclideanSpace.volume_closedBall, gaussSum_sq, SimpleGraph.card_cliqueFinset_le, card_embedding_eq, Set.card_insert, AlternatingGroup.card_of_cycleType_mul_eq, SimpleGraph.edgeFinset_card, zpow_mod_card, IsKleinFour.card_four', ZMod.card, SimpleGraph.Coloring.colorable, jacobiSum_one_one, card_eq_nat_card, Set.Intersecting.exists_card_eq, hammingDist_le_card_fintype, SimpleGraph.bot_strongly_regular, RCLike.wInner_cWeight_eq_smul_wInner_one, MeasureTheory.volume_sum_rpow_lt_one, SimpleGraph.card_topEdgeLabeling, one_dotProduct_one, Equiv.Perm.card_isConj_mul_eq, SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective, Matrix.permanent_smul, Submonoid.eq_bot_iff_card, Nat.card_eq_fintype_card, Algebra.Norm.Transitivity.det_mul_corner_pow, Equiv.Perm.nat_card_centralizer, Set.Intersecting.card_le, card_sum, SimpleGraph.Walk.IsHamiltonian.length_support, modularCyclotomicCharacter.toFun_spec'', card_le_of_surjective, ContinuousAlternatingMap.norm_image_sub_le, SimpleGraph.maxDegree_lt_card_verts, SimpleGraph.colorable_of_fintype, Module.finrank_finsupp, Matrix.SpecialLinearGroup.mem_center_iff, Encodable.length_sortedUniv, Set.Sized.card_le, card_lt_of_injective_not_surjective, card_zmultiples_le, card_le_one_iff_subsingleton, SimpleGraph.IsTree.card_edgeFinset, card_subtype_eq, card_linearIndependent, card_bool, FinEnum.card_eq_fintypeCard, linearIndependent_iff_card_eq_finrank_span, expect_eq_sum_div_card, Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
|