Fintype 📖 | CompData | 38 mathmath: Finset.doubling_lt_three_halves, AddCommGroup.equiv_directSum_zmod_of_finite', Combinatorics.Line.exists_mono_in_high_dimension, Module.equiv_directSum_of_isTorsion, exists_birkhoff_representation, CommGroup.equiv_prod_multiplicative_zmod_of_finite, Fintype.subsingleton, AddCommGroup.equiv_free_prod_directSum_zmod, CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen, Algebra.FiniteType.iff_quotient_mvPolynomial', AddCommGroup.equiv_directSum_zmod_of_finite, Finite.exists_type_univ_nonempty_addEquiv, eq_pos_convex_span_of_mem_convexHull, Finset.doubling_lt_two, Finset.doubling_lt_golden_ratio, IsLiouville.isLiouville, Submodule.exists_isInternal_prime_power_torsion_of_pid, Combinatorics.Subspace.exists_mono_in_high_dimension, CommGroup.equiv_free_prod_prod_multiplicative_zmod, nonempty_fintype, Fintype.instFastSubsingleton, exists_signed_sum', Algebra.FiniteType.iff_quotient_freeAlgebra', Module.equiv_free_prod_directSum, Cardinal.mk_eq_nat_iff_fintype, finite_iff_nonempty_fintype, Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0, mem_convexHull_iff_exists_fintype, Set.Finite.nonempty_fintype, Finset.card_mul_finset_lt_two, Set.finite_def, Language.isRegular_iff, exists_signed_sum, Finite.exists_type_univ_nonempty_mulEquiv, isEmpty_fintype, Set.univ_finite_iff_nonempty_fintype, Cardinal.lt_aleph0_iff_fintype, Algebra.FinitePresentation.iff_quotient_mvPolynomial'
|