Documentation Verification Report

IsCoprime

📁 Source: Mathlib/Tactic/NormNum/IsCoprime.lean

Statistics

Metric	Count
Definitions `IsCoprime`, `evalIntIsCoprime`, `proveIntIsCoprime`	3
Theorems `int_not_isCoprime_helper`, `isInt_isCoprime`, `isInt_not_isCoprime`	3
Total	6

Tactic.NormNum

Definitions

Name	Category	Theorems
`evalIntIsCoprime` 📖	CompOp	—
`proveIntIsCoprime` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`int_not_isCoprime_helper` 📖	mathematical	—	`IsCoprime` `Int.instCommSemiring`	—	`Int.isCoprime_iff_gcd_eq_one`
`isInt_isCoprime` 📖	—	`Mathlib.Meta.NormNum.IsInt` `Int.instRing` `IsCoprime` `Int.instCommSemiring`	—	—	—
`isInt_not_isCoprime` 📖	—	`Mathlib.Meta.NormNum.IsInt` `Int.instRing` `IsCoprime` `Int.instCommSemiring`	—	—	—

(root)

Definitions

Name	Category	Theorems
`IsCoprime` 📖	MathDef	111 math math: `Padic.norm_intCast_eq_one_iff`, `isCoprime_comm`, `IsCoprime.mul_add_left_right_iff`, `Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero`, `ModularGroup.bottom_row_coprime`, `IsCoprime.add_mul_right_left_iff`, `IsCoprime.abs_right_iff`, `Int.isCoprime_iff_nat_coprime`, `Zsqrtd.exists_coprime_of_gcd_pos`, `Prime.coprime_iff_not_dvd`, `ModularGroup.bottom_row_surj`, `Int.isCoprime_iff_gcd_eq_one`, `Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd`, `RatFunc.isCoprime_num_denom`, `Ideal.sup_eq_top_iff_isCoprime`, `IsCoprime.pow_left_iff`, `pairwise_coprime_iff_coprime_prod`, `dvd_or_isCoprime`, `Rat.isCoprime_num_den`, `isCoprime_group_smul_right`, `Ideal.isCoprime_iff_gcd`, `isCoprime_mul_unit_right_right`, `isCoprime_mul_unit_left_left`, `IsCoprime.add_mul_right_right_iff`, `IsCoprime.neg_right_iff`, `Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst`, `Matrix.SpecialLinearGroup.isCoprime_col`, `IsRelPrime.isCoprime`, `not_isCoprime_zero_zero`, `isCoprime_group_smul_left`, `isCoprime_of_prime_dvd`, `IsCoprime.prod_right_iff`, `isCoprime_mul_unit_left`, `Polynomial.isCoprime_expand`, `exists_sum_eq_one_iff_pairwise_coprime'`, `Matrix.SpecialLinearGroup.isCoprime_row`, `IsCoprime.mul_add_left_left_iff`, `Polynomial.isUnit_resultant_iff_isCoprime`, `EuclideanDomain.isCoprime_of_dvd`, `EisensteinSeries.finGcdMap_div`, `IsCoprime.add_mul_left_right_iff`, `isCoprime_mul_unit_right_left`, `Polynomial.cyclotomic.isCoprime_rat`, `isCoprime_zero_left`, `isCoprime_group_smul`, `Semifield.isCoprime_iff`, `isCoprime_of_dvd`, `isCoprime_div_gcd_div_gcd`, `isCoprime_of_irreducible_dvd`, `isCoprime_mul_unit_right`, `Ideal.isCoprime_tfae`, `isCoprime_self`, `ZMod.coe_int_isUnit_iff_isCoprime`, `Polynomial.natSepDegree_mul_eq_iff`, `Nat.isCoprime_iff_coprime`, `PadicInt.norm_intCast_eq_one_iff`, `IsCoprime.mul_right_iff`, `Ideal.isCoprime_iff_exists`, `Polynomial.separable_def`, `IsCoprime.mul_add_right_right_iff`, `Irreducible.dvd_iff_not_isCoprime`, `IsCoprime.pow_right_iff`, `gcd_isUnit_iff`, `IsCoprime.abs_left_iff`, `EuclideanDomain.gcd_isUnit_iff`, `Ideal.coprime_of_no_prime_ge`, `Polynomial.Separable.isCoprime`, `isCoprime_one_right`, `isCoprime_mul_unit_left_right`, `isCoprime_mul_units_left`, `Irreducible.isCoprime_or_dvd`, `Irreducible.coprime_pow_of_not_dvd`, `isRelPrime_iff_isCoprime`, `Ideal.isCoprime_span_singleton_iff`, `FermatLastTheoremForThreeGen.Solution'.coprime`, `isCoprime_zero_right`, `Ideal.isCoprime_iff_add`, `isCoprime_of_gcd_eq_one_of_FLT`, `IsCoprime.neg_left_iff`, `IsCoprime.pow_iff`, `isCoprime_mul_units_right`, `IsCoprime.abs_abs_iff`, `Polynomial.isCoprime_map`, `Nat.Coprime.cast`, `IsCoprime.neg_neg_iff`, `exists_sum_eq_one_iff_pairwise_coprime`, `IsPrimitiveRoot.arg`, `Fermat42.coprime_of_minimal`, `IsCoprime.prod_left_iff`, `Ideal.isCoprime_iff_codisjoint`, `Ideal.isCoprime_iff_sup_eq`, `IsCoprime.mul_left_iff`, `Tactic.NormNum.int_not_isCoprime_helper`, `Ideal.isCoprime_of_isMaximal`, `Polynomial.resultant_eq_zero_iff`, `isCoprime_div_gcd_div_gcd_of_gcd_ne_zero`, `Nat.isCoprime_iff`, `IsCoprime.add_mul_left_left_iff`, `Polynomial.pairwise_coprime_X_sub_C`, `PNat.isCoprime_iff`, `EuclideanDomain.dvd_or_coprime`, `Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂`, `isCoprime_one_left`, `Polynomial.isCoprime_iff_aeval_ne_zero`, `FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd`, `Irreducible.coprime_iff_not_dvd`, `Polynomial.isCoprime_X_sub_C_of_isUnit_sub`, `IsCoprime.mul_add_right_left_iff`, `Nat.Coprime.isCoprime`, `EisensteinSeries.mem_gammaSet_one`, `Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed`

---

← Back to Index