card 📖 | CompOp | 428 mathmath: Subgroup.card_map_of_injective, FiniteField.Extension.frob_apply, Subgroup.card_eq_card_quotient_mul_card_subgroup, orderOf_lt_card, AddSubmonoid.addOrderOf_le_card, IsOfFinOrder.natCard_powers_le_orderOf, Subgroup.index_center_le_pow, orderOf_eq_card_of_forall_mem_zpowers, card_le_card_of_injective, IsGalois.card_aut_eq_finrank, MulAction.IsBlock.ncard_dvd_card, CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso, card_units, Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite, Set.natCard_smul_set₀, NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two, NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, AddSubgroup.IsComplement.card_mul_card, IsCyclic.val_mulAutMulEquiv_apply, Subgroup.card_top, AddSubgroup.card_map_of_injective, AddAction.IsBlock.ncard_block_add_ncard_orbit_eq, AddSubgroup.card_comap_dvd_of_injective, cyclotomicCharacter.toZModPow, IsZGroup.coprime_commutator_index, AlgHom.IsArithFrobAt.mk_apply, Field.finSepDegree_eq_of_isAlgClosed, IsGalois.card_fixingSubgroup_eq_finrank, Set.Finite.card_lt_card, SubMulAction.nat_card_ofStabilizer_add_one_eq, Sylow.card_dvd_index, ModularForm.norm_eq_zero_iff, CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected, card_zmultiples, AddSubgroup.card_eq_iff_eq_top, AddSubgroup.IsComplement.card_right, Finite.card_subtype_le, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, card_eq_finsetCard, card_dvd_exponent_pow_rank, NumberField.InfinitePlace.card_stabilizer, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, IsAddCyclic.index_nsmulAddMonoidHom_range, Subgroup.exists_left_transversal_of_le, Subgroup.one_lt_card_iff_ne_bot, Subgroup.card_le_of_le, AddSubgroup.card_dvd_of_injective, Subgroup.card_eq_one, AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup, Subgroup.IsComplement'.index_eq_card, IsAddCyclic.exists_ofOrder_eq_natCard, card_comm_eq_card_conjClasses_mul_card, card_le_card_of_surjective, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, orderOf_eq_card_of_forall_mem_powers, card_pos, Subgroup.card_bot, IteratedWreathProduct.card, card_of_subsingleton, orderOf_le_card, DihedralGroup.card_commute_odd, RegularWreathProduct.card, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum, card_eq_zero_of_infinite, Subgroup.rank_closure_finite_le_nat_card, tendsto_card_div_pow_atTop_volume, IsPGroup.coprime_card_of_ne, AddSubgroup.card_range_dvd, card_perm, MulAction.index_stabilizer_of_transitive, CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, isCyclic_iff_exists_natCard_le_orderOf, AddSubgroup.card_subtype, IsPGroup.iff_card, MonoidHom.not_dvd_card_ker_transferSylow, Set.natCard_add_le, HasEnoughRootsOfUnity.natCard_rootsOfUnity, Set.ncard_le_card, ZLattice.covolume.tendsto_card_div_pow, AddGroup.is_simple_iff_prime_card, FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard, FiniteField.algebraMap_trace_eq_sum_pow, Subgroup.index_ker, Monoid.minOrder_le_natCard, Matrix.card_GL_field, Subgroup.eq_bot_iff_card, SimpleGraph.ConnectedComponent.card_le_card_of_le, Set.ncard_lt_card, Set.powersetCard.nontrivial_iff, SubAddAction.ofFixingAddSubgroup.append_left, AddSubgroup.index_ker, pow_mod_natCard, card_sum, IsPGroup.exists_card_eq, Projectivization.card'', SemidirectProduct.card, Polynomial.Gal.prime_degree_dvd_card, Ideal.card_stabilizer_eq, card_eq_two_iff', Subgroup.index_mul_card, AddSubgroup.card_le_of_le, orderOf_dvd_natCard, Finset.card_preimage_eq_sum_card_image_eq, Subgroup.card_commutator_le_of_finite_commutatorSet, AddSubgroup.index_dvd_card, Set.ncard_compl, card_image_of_injective, Subgroup.card_dvd_of_injective, NumberField.InfinitePlace.even_card_aut_of_not_isUnramified, Set.card_union_le, AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotient, Set.powersetCard.eq_empty_iff, IsCyclic.exists_ofOrder_eq_natCard, Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator, AddGroup.isAddCyclic_prod_iff, card_commutatorSet_closureCommutatorRepresentatives, IsCyclic.val_inv_mulAutMulEquiv_apply, IsOfFinAddOrder.natCard_multiples_le_addOrderOf, IsAddCyclic.image_range_card, Equiv.Perm.card_isConj_eq, AlgHom.IsArithFrobAt.apply_of_pow_eq_one, FiniteField.pow_finrank_eq_natCard, Finite.card_le_of_surjective, card_preimage_of_injOn, AddSubgroup.rank_closure_finite_le_nat_card, Subgroup.IsComplement'.card_mul, SimpleGraph.isTree_iff_connected_and_card, Subgroup.card_dvd_of_surjective, AddSubgroup.card_dvd_of_le, Subgroup.card_range_dvd, FiniteField.algebraMap_norm_eq_pow, card_nsmul_eq_zero', Finite.card_eq_zero_iff, CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso, coprime_card_of_isCyclic_prod, SubMulAction.nat_card_ofStabilizer_eq, AddSubgroup.card_mul_index, FiniteField.algebraMap_norm_eq_prod_pow, Subgroup.rank_commutator_le_card, card_univ, AddSubgroup.card_addSubgroup_dvd_card, card_of_isEmpty, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, card_coe_set_eq, IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank, Submodule.card_quotient_mul_card_quotient, AddCircle.card_addOrderOf_eq_totient, card_pos_iff, IsAddCyclic.card_nsmulAddMonoidHom_ker, card_submonoidPowers, Finite.card_sum, Set.natCard_pos, Subgroup.card_map_dvd, IsPGroup.card_modEq_card_fixedPoints, IsCyclic.card_powMonoidHom_ker, Set.sum_indicator_eventually_eq_card, Finite.card_subtype_lt, ModN.natCard_eq, isCyclic_iff_exists_orderOf_eq_natCard, Subgroup.relIndex_bot_left, addOrderOf_eq_card_of_forall_mem_multiples, AddSubgroup.index_mul_card, Finite.card_image_le, IsPGroup.nontrivial_iff_card, pow_card_eq_one', IsPGroup.card_orbit, Set.ncard_add_ncard_compl, Subgroup.card_commutator_dvd_index_center_pow, bijective_iff_injective_and_card, NumberField.Ideal.tendsto_norm_le_div_atTop₀, Set.Nonempty.natCard_pos, Submodule.natAbs_det_equiv, AddSubgroup.card_le_one_iff_eq_bot, addOrderOf_dvd_natCard, addOrderOf_le_card, card_eq_of_equiv_fin, Set.natCard_smul_set, Projectivization.card, Finite.card_pos, FiniteField.splits_X_pow_nat_card_sub_X, ZLattice.covolume.tendsto_card_le_div', subtype_card, SubMulAction.nat_card_ofStabilizer_eq_add_one, DihedralGroup.nat_card, Set.card_singleton_prod, AlgHom.natCard_of_splits, SubAddAction.nat_card_ofStabilizer_eq, Module.natCard_eq_pow_finrank, card_addSubmonoidMultiples, SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one, Subgroup.index_bot, Set.card_prod_singleton, card_eq_one_iff_unique, AddSubgroup.card_top, Subgroup.IsComplement.card_mul_card, card_dvd_exponent_pow_rank', IsCyclic.card_mulAut, card_fun, NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two, Ideal.card_norm_le_eq_card_norm_le_add_one, CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected, card_eq_card_units_add_one, card_dvd_exponent_nsmul_rank, bijective_iff_surjective_and_card, tprod_const, IsAddCyclic.iff_exponent_eq_card, card_mono, Set.natCard_inv, RootPairing.EmbeddedG2.card_index_eq_twelve, Function.Surjective.card_le_card_add_one_iff, Group.is_simple_iff_prime_card, card_image_of_injOn, isNilpotent_of_finite_tfae, Subgroup.card_le_card_group, addOrderOf_eq_card_of_forall_mem_zmultiples, Finite.card_le_one_iff_subsingleton, isZGroup_iff_exists_mulEquiv, card_eq, SimpleGraph.Colorable.card_le_of_pairwise_adj, AddMonoid.le_minOrder_iff_forall_addSubgroup, card_congr, IntermediateField.card_algHom_adjoin_integral, AddAction.index_stabilizer_of_transitive, AddSubgroup.card_map_dvd, Subgroup.IsComplement.card_right, IsCyclic.image_range_card, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, IsCyclic.index_powMonoidHom_ker, Sylow.card_eq_multiplicity, MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self, AlternatingGroup.isMultiplyPretransitive, addOrderOf_eq_card_of_zmultiples_eq_top, Set.natCard_vadd_set, Projectivization.card_of_finrank, cast_card, ZLattice.covolume.tendsto_card_div_pow', Subgroup.card_subgroup_dvd_card, AddGroup.exponent_dvd_nat_card, Set.natCard_neg, card_plift, Finite.card_pos_iff, card_eq_two_iff, IsCyclic.iff_exponent_eq_card, Subgroup.card_quotient_dvd_card, SubMulAction.ofFixingSubgroup.append_left, LinearMap.equivariantProjection_apply, Monoid.le_minOrder_iff_forall_subgroup, FiniteField.natCard_extension, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq, AddAction.IsBlock.ncard_dvd_card, Module.finrank_eq_nat_card_basis, AddSubgroup.addOrderOf_dvd_natCard, card_sigma, ZLattice.covolume.tendsto_card_le_div, Subgroup.IsComplement.card_left, Projectivization.card', AlgHom.IsArithFrobAt.card_pos, AddSubgroup.card_bot, IsCyclic.index_powMonoidHom_range, card_zpowers, IntermediateField.finrank_fixedField_eq_card, IsPrimitiveRoot.card_quotient_toInteger_sub_one, two_mul_nat_card_alternatingGroup, NumberField.Ideal.tendsto_norm_le_div_atTop, Ideal.card_inertia_eq_ramificationIdxIn, Subgroup.card_dvd_of_le, orderOf_eq_card_of_zpowers_eq_top, NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, Group.exponent_dvd_nat_card, Subgroup.isComplement'_iff_card_mul_and_disjoint, card_commutator_closureCommutatorRepresentatives, card_pi, FiniteField.natCard_algHom_of_finrank_dvd, IsZGroup.exponent_eq_card, IsCyclic.exponent_eq_card, AlgHom.natCard_of_powerBasis, Subgroup.index_eq_card, MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity, AddSubgroup.one_lt_card_iff_ne_bot, NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified, card_prod, cyclotomicCharacter.toZModPow_toFun, Subgroup.exists_right_transversal_of_le, card_sylow_modEq_one, IsSimpleGroup.prime_card, MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq, Finite.one_lt_card, IsSimpleAddGroup.prime_card, IsAddKleinFour.card_four, card_eq_card_toFinset, Set.natCard_mul_le, card_image_equiv, GaloisField.card, isAddCyclic_iff_exists_addOrderOf_eq_natCard, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, ModularForm.coe_norm, Ideal.card_stabilizer_eq_card_inertia_mul_finrank, IsGalois.of_separable_splitting_field_aux, Set.eq_univ_iff_ncard, Finite.card_le_of_injective, MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self, DihedralGroup.card_conjClasses_odd, SimpleGraph.odd_ncard_oddComponents, Finite.card_le_of_embedding, CommGroup.is_simple_iff_isCyclic_and_prime_card, Set.powersetCard.card, card_unique, Set.natCard_graphOn, mod_natCard_nsmul, card_ulift, QuotientGroup.card_preimage_mk, AddSubgroup.index_range, CommGroup.is_simple_iff_prime_card, alternatingGroup.isMultiplyPretransitive, DirichletCharacter.card_eq_totient_of_hasEnoughRootsOfUnity, IsCyclic.mulAutMulEquiv_symm_apply_apply, AddCommGroup.is_simple_iff_prime_card, AddSubgroup.index_eq_card, ZLattice.covolume.tendsto_card_le_div'', MonoidHom.FixedPointFree.odd_card_of_involutive, card_zmod, mod_natCard_zsmul, isAddCyclic_iff_exists_natCard_le_addOrderOf, Finite.card_option, Subgroup.card_le_one_iff_eq_bot, tendsto_card_div_pow_atTop_volume', AddSubgroup.exists_right_transversal_of_le, Subgroup.card_subtype, SubAddAction.nat_card_ofStabilizer_add_zero_eq, Ideal.ncard_primesOver_mul_card_inertia_mul_finrank, card_algHom_le_finrank, commProb_def', Set.natCard_div_le, Subgroup.card_mul_eq_card_subgroup_mul_card_quotient, card_image_le, not_dvd_card_sylow, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, rank_closureCommutatorRepresentatives_le, AddSubgroup.card_eq_one, AddSubgroup.eq_bot_iff_card, Subgroup.orderOf_le_card, tsum_const, Subgroup.relIndex_ker, IsGaloisGroup.card_eq_finrank, IsGalois.tfae, Subfield.card_bot, card_eq_one_iff_exists, card_dvd_exponent_nsmul_rank', Set.ncard_univ, Finite.card_eq, NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn, AddSubgroup.card_le_card_addGroup, Projectivization.card_of_finrank_two, Group.isCyclic_prod_iff, Subgroup.orderOf_dvd_natCard, MvPolynomial.ringKrullDim_of_isNoetherianRing, IsCyclic.card_powMonoidHom_range, Subgroup.card_mul_index, Finite.card_range_le, AddSubgroup.exists_left_transversal_of_le, Group.nat_card_center_add_sum_card_noncenter_eq_card, totient_eq_card_lt_and_coprime, Sylow.card_eq_card_quotient_normalizer, Field.finSepDegree_eq_of_adjoin_splits, IsGaloisGroup.card_fixingSubgroup_eq_finrank, card_eq_of_bijective, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, Subgroup.IsComplement.card_mul, AddSubgroup.IsComplement.card_left, Set.Infinite.card_eq_zero, Subgroup.index_range, IsAddCyclic.index_nsmulAddMonoidHom_ker, nat_card_alternatingGroup, ZLattice.covolume.tendsto_card_div_pow'', card_preimage_of_injective, IsKleinFour.card_four, Subgroup.commProb_quotient_le, AddSubgroup.relIndex_ker, Polynomial.Gal.card_of_separable, Subgroup.relIndex_dvd_card, zpow_mod_natCard, AddSubgroup.card_quotient_dvd_card, FiniteField.algebraMap_norm_eq_pow_sum, AddSubgroup.relIndex_dvd_card, AddSubgroup.addOrderOf_le_card, Set.ncard_range_of_injective, FiniteField.natCard_algEquiv_extension, card_fin, commProb_def, Subgroup.nat_card_centralizer_nat_card_stabilizer, card_eq_zero, Finite.one_lt_card_iff_nontrivial, AddMonoid.minOrder_le_natCard, Fintype.card_eq_nat_card, Group.sum_card_conj_classes_eq_card, SlashInvariantForm.coe_norm, inv_card_commutator_le_commProb, Equiv.Perm.card_isConj_mul_eq, Sylow.card_eq_index_normalizer, card_eq_fintype_card, Equiv.Perm.nat_card_centralizer, Subgroup.card_eq_iff_eq_top, AddSubgroup.index_bot, Submonoid.orderOf_le_card, IsAddCyclic.exponent_eq_card, IsPGroup.card_eq_or_dvd, Set.natCard_sub_le, coprime_card_of_isAddCyclic_prod, AlgHom.IsArithFrobAt.restrict_apply, natCard_units_lt, card_range_of_injective, FDRep.simple_iff_char_is_norm_one, ENat.card_eq_coe_natCard, AddSubgroup.card_dvd_of_surjective, AddSubgroup.relIndex_bot_left, Sylow.card_coprime_index, MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul, Submodule.card_eq_card_quotient_mul_card, card_subtype_true, IsAddCyclic.card_nsmulAddMonoidHom_range, card_linearIndependent, Submodule.natAbs_det_basis_change, Submodule.cardQuot_apply, Subgroup.card_comap_dvd_of_injective, card_eq_card_finite_toFinset, Subgroup.index_dvd_card
|