| Metric | Count |
|---|
DefinitionsIsRadical, finsuppTotal, instIdemCommSemiring, radical, radicalInfTopHom, uniqueUnits, algebraIdeal, mapAlgEquiv, mapAlgHom, moduleSubmodule | 10 |
Theoremsmk_ne_zero', mem_ideal_span_range_iff_exists_finsupp, inf_le, inf_le', isRadical, le_of_pow_le, mul_le, multiset_prod_le, multiset_prod_map_le, multiset_prod_mem_iff_exists_mem, notMem_of_isCoprime_of_mem, pow_le_iff, prod_le, prod_mem_iff, prod_mem_iff_exists_mem, radical, radical_le_iff, inf, radical, radical_le_iff, instHMul, instHPowNat, mul_one, pow_add, pow_succ, add_eq_one_iff, add_eq_sup, bot_mul, bot_pow, coprime_of_no_prime_ge, disjoint_powers_iff_notMem, dvd_bot, eq_inf_of_isPrime_inf, eq_span_singleton_mul, exists_subset_radical_span_sup_of_subset_radical_sup, finset_inf_span_singleton, finsuppTotal_apply, finsuppTotal_apply_eq_of_fintype, iInf_span_singleton, iInf_span_singleton_natCast, iInf_sup_eq_top, iSup_mul, inf_eq_mul_of_isCoprime, instIsTorsionFreeSubtypeMemSubmodule, instNoZeroDivisors, isCoprime_biInf, isCoprime_iff_add, isCoprime_iff_codisjoint, isCoprime_iff_exists, isCoprime_iff_sup_eq, isCoprime_of_isMaximal, isCoprime_span_singleton_iff, isCoprime_tfae, isRadical_bot, isRadical_bot_iff, isRadical_bot_of_noZeroDivisors, isRadical_iInf, isRadical_iff_pow_one_lt, isUnit_iff, le_of_dvd, le_radical, le_span_singleton_mul_iff, mem_mul_span_singleton, mem_radical_iff, mem_radical_of_pow_mem, mem_span_range_iff_exists_fun, mem_span_singleton_mul, mul_assoc, mul_bot, mul_comm, mul_eq_bot, mul_eq_inf_of_coprime, mul_iSup, mul_le, mul_le_inf, mul_le_left, mul_le_right, mul_left_self_sup, mul_mem_mul, mul_mem_mul_rev, mul_mono, mul_mono_left, mul_mono_right, mul_right_self_sup, mul_sup, mul_sup_eq_of_coprime_left, mul_sup_eq_of_coprime_right, mul_top, multiset_prod_eq_bot, multiset_prod_le_inf, multiset_prod_span_singleton, natCast_eq_top, ofNat_eq_top, one_eq_top, pow_eq_top_iff, pow_eq_zero_of_mem, pow_le_pow_right, pow_le_self, pow_mem_pow, pow_right_mono, pow_sup_eq_top, pow_sup_eq_top', pow_sup_pow_eq_top, pow_sup_pow_eq_top', primeCompl_le_nonZeroDivisors, prod_le_inf, prod_mem_prod, prod_span, prod_span_singleton, prod_sup_eq_top, radicalInfTopHom_apply, radical_bot_of_noZeroDivisors, radical_eq_iff, radical_eq_sInf, radical_eq_top, radical_finset_inf, radical_iInf_le, radical_idem, radical_inf, radical_isRadical, radical_le_radical_iff, radical_mono, radical_mul, radical_pow, radical_sup, radical_top, range_finsuppTotal, range_mul, range_mul', smul_eq_mul, span_mul_span, span_mul_span', span_pair_mul_span_pair, span_singleton_mul_eq_span_singleton_mul, span_singleton_mul_le_iff, span_singleton_mul_le_span_singleton_mul, span_singleton_mul_left_inj, span_singleton_mul_left_injective, span_singleton_mul_left_mono, span_singleton_mul_right_inj, span_singleton_mul_right_injective, span_singleton_mul_right_mono, span_singleton_mul_span_singleton, span_singleton_nonZeroDivisors, span_singleton_pow, span_singleton_toAddSubgroup_eq_zmultiples, subset_union, subset_union_prime, subset_union_prime', subset_union_prime_finite, sum_eq_sup, sup_eq_top_iff_isCoprime, sup_iInf_eq_top, sup_mul, sup_mul_eq_of_coprime_left, sup_mul_eq_of_coprime_right, sup_mul_left_self, sup_mul_right_self, sup_multiset_prod_eq_top, sup_pow_add_le_pow_sup_pow, sup_pow_eq_top, sup_pow_eq_top', sup_prod_eq_top, top_mul, top_pow, zero_eq_bot, add_eq, codisjoint, exists, sup_eq, coe_mapAlgEquiv_apply, coe_mapAlgEquiv_symm_apply, coe_mapAlgHom_apply, coe_span_smul, comap_smul'', ideal_span_singleton_smul, map_le_smul_top, map_pointwise_smul, map_smul'', mem_ideal_smul_span_iff_exists_sum, mem_ideal_smul_span_iff_exists_sum', mem_of_span_eq_top_of_smul_pow_mem, mem_of_span_top_of_smul_mem, mem_smul_span, mem_smul_span_singleton, mem_smul_top_iff, mul_smul, set_smul_top_eq_span, smul_comap_le_comap_smul, smul_eq_map₂, smul_le_right, smul_le_span, span_singleton_toAddSubgroup_eq_zmultiples, span_smul_eq, span_smul_span, top_smul, instNonUnitalSubringClassIdeal, instNonUnitalSubsemiringClassIdeal | 198 |
| Total | 208 |