| Metric | Count |
|---|
DefinitionsinstGCDMonoid, out, instNormalizedGCDMonoid, gcd, lcm, NormalizationMonoid, normUnit, ofUniqueUnits, NormalizedGCDMonoid, toGCDMonoid, toNormalizationMonoid, associatesEquivOfUniqueUnits, gcdMonoidOfExistsGCD, gcdMonoidOfExistsLCM, gcdMonoidOfGCD, gcdMonoidOfLCM, normalizationMonoidOfMonoidHomRightInverse, normalize, normalizedGCDMonoidOfExistsGCD, normalizedGCDMonoidOfExistsLCM, normalizedGCDMonoidOfGCD, normalizedGCDMonoidOfLCM, uniqueNormalizationMonoidOfUniqueUnits | 23 |
Theoremseq_of_normalized, gcd, gcd_eq_left, gcd_eq_right, lcm, dvd_out_iff, gcd_mk_mk, lcm_mk_mk, mk_normalize, mk_out, normalize_out, out_dvd_iff, out_eq_zero_iff, out_injective, out_mk, out_mul, out_one, out_top, out_zero, coe_normUnit, normalize_eq_one, lcm_left, lcm_right, dvd_gcd, gcd_dvd_left, gcd_dvd_right, gcd_mul_lcm, lcm_zero_left, lcm_zero_right, toIsCancelMulZero, gcd_eq_one_iff, isUnit_gcd_iff, normUnit_coe_units, normUnit_mul, normUnit_zero, normalize_gcd, normalize_lcm, dvd_lcm, dvd_or_dvd_of_dvd_lcm, not_dvd_lcm, associated_gcd_left_iff, associated_gcd_right_iff, associated_normalize, associated_normalize_iff, associatesEquivOfUniqueUnits_apply, associatesEquivOfUniqueUnits_symm_apply, dvd_antisymm_of_normalize_eq, dvd_gcd_iff, dvd_gcd_mul_iff_dvd_mul, dvd_gcd_mul_of_dvd_mul, dvd_lcm_left, dvd_lcm_of_dvd_left, dvd_lcm_of_dvd_right, dvd_lcm_right, dvd_mul_gcd_iff_dvd_mul, dvd_mul_gcd_of_dvd_mul, dvd_normalize_iff, dvd_of_lcm_left_dvd, dvd_of_lcm_right_dvd, exists_associated_pow_of_mul_eq_pow, exists_eq_pow_of_mul_eq_pow, extract_gcd, gcd_assoc, gcd_assoc', gcd_comm, gcd_comm', gcd_dvd_gcd, gcd_dvd_gcd_mul_left, gcd_dvd_gcd_mul_left_right, gcd_dvd_gcd_mul_right, gcd_dvd_gcd_mul_right_right, gcd_eq_left_iff, gcd_eq_normalize, gcd_eq_of_dvd_sub_left, gcd_eq_of_dvd_sub_right, gcd_eq_right_iff, gcd_eq_zero_iff, gcd_greatest, gcd_greatest_associated, gcd_isUnit_iff_isRelPrime, gcd_mul_dvd_mul_gcd, gcd_mul_lcm, gcd_mul_left, gcd_mul_left', gcd_mul_right, gcd_mul_right', gcd_ne_zero_of_left, gcd_ne_zero_of_right, gcd_neg, gcd_neg', gcd_one_left, gcd_one_left', gcd_one_right, gcd_one_right', gcd_pow_left_dvd_pow_gcd, gcd_pow_right_dvd_pow_gcd, gcd_same, gcd_zero_left, gcd_zero_left', gcd_zero_right, gcd_zero_right', instAssociativeGcd, instAssociativeLcm, instCommutativeGcd, instCommutativeLcm, instDecompositionMonoidOfNonemptyGCDMonoid, instNonemptyGCDMonoid, instNonemptyGCDMonoidOfNormalizedGCDMonoid, instNonemptyNormalizationMonoid, instNonemptyNormalizationMonoidOfNormalizedGCDMonoid, instNonemptyNormalizedGCDMonoid, isUnit_gcd_of_eq_mul_gcd, isUnit_gcd_one_left, isUnit_gcd_one_right, lcm_assoc, lcm_assoc', lcm_comm, lcm_comm', lcm_dvd, lcm_dvd_iff, lcm_dvd_lcm, lcm_dvd_lcm_mul_left, lcm_dvd_lcm_mul_left_right, lcm_dvd_lcm_mul_right, lcm_dvd_lcm_mul_right_right, lcm_dvd_mul, lcm_eq_left_iff, lcm_eq_normalize, lcm_eq_of_associated_left, lcm_eq_of_associated_right, lcm_eq_one_iff, lcm_eq_right_iff, lcm_eq_zero_iff, lcm_mul_left, lcm_mul_right, lcm_one_left, lcm_one_right, lcm_same, lcm_units_coe_left, lcm_units_coe_right, neg_gcd, neg_gcd', normUnit_eq_one, normUnit_mul_normUnit, normUnit_one, normalize_apply, normalize_associated, normalize_associated_iff, normalize_coe_units, normalize_dvd_iff, normalize_eq, normalize_eq_normalize, normalize_eq_normalize_iff, normalize_eq_normalize_iff_associated, normalize_eq_one, normalize_eq_zero, normalize_gcd, normalize_idem, normalize_lcm, normalize_one, normalize_zero, pow_dvd_of_mul_eq_pow, subsingleton_gcdMonoid_of_unique_units, subsingleton_normalizedGCDMonoid_of_unique_units | 164 |
| Total | 187 |