Documentation Verification Report

GCD

📁 Source: Mathlib/Data/Int/GCD.lean

Statistics

Metric	Count
Definitions `gcdA`, `gcdB`, `gcdA`, `gcdB`, `xgcd`, `xgcdAux`	6
Theorems `pow_eq_pow_iff_of_coprime`, `dvd_of_dvd_mul_left_of_gcd_one`, `dvd_of_dvd_mul_right_of_gcd_one`, `exists_gcd_one`, `exists_gcd_one'`, `gcd_def`, `gcd_div`, `gcd_div_gcd_div_gcd`, `gcd_dvd_iff`, `gcd_eq_gcd_ab`, `gcd_eq_one_of_gcd_mul_right_eq_one_left`, `gcd_eq_one_of_gcd_mul_right_eq_one_right`, `gcd_greatest`, `gcd_least_linear`, `lcm_def`, `ne_zero_of_gcd`, `exists_mul_emod_eq_gcd`, `exists_mul_emod_eq_one_of_coprime`, `exists_mul_mod_eq_gcd`, `exists_mul_mod_eq_of_coprime`, `exists_mul_mod_eq_one_of_coprime`, `gcdA_zero_left`, `gcdA_zero_right`, `gcdB_zero_left`, `gcdB_zero_right`, `gcd_eq_gcd_ab`, `xgcdAux_fst`, `xgcdAux_rec`, `xgcdAux_val`, `xgcd_val`, `xgcd_zero_left`, `gcd_nsmul_eq_zero`, `intGCD_nsmul_eq_zero`, `nsmul_eq_zero_iff_of_coprime`, `pow_eq_one_iff_of_coprime`, `pow_eq_pow_iff_of_coprime`, `pow_gcd_eq_one`, `pow_intGCD_eq_one`, `pow_mem_range_pow_of_coprime`	39
Total	45

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_eq_pow_iff_of_coprime` 📖	mathematical	`Commute` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Monoid.toNatPow` `MonoidWithZero.toMonoid`	—	`pow_one` `pow_zero` `zero_pow` `isReduced_of_noZeroDivisors` `GroupWithZero.noZeroDivisors` `zpow_natCast` `Nat.gcd_eq_gcd_ab` `zpow_add₀` `mul_zpow` `zpow_zpow₀` `mul_comm` `zpow_mul` `symm` `pow_pow` `pow_mul` `pow_mul'`

Int

Definitions

Name	Category	Theorems
`gcdA` 📖	CompOp	2 math math: `gcd_eq_gcd_ab`, `isCoprime_gcdA`
`gcdB` 📖	CompOp	2 math math: `isCoprime_gcdB`, `gcd_eq_gcd_ab`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_dvd_mul_left_of_gcd_one` 📖	—	—	—	—	`gcd_eq_gcd_ab` `mul_assoc` `zero_add` `mul_one` `dvd_mul_left`
`dvd_of_dvd_mul_right_of_gcd_one` 📖	—	—	—	—	`dvd_of_dvd_mul_left_of_gcd_one` `mul_comm`
`exists_gcd_one` 📖	—	—	—	—	`gcd_div_gcd_div_gcd`
`exists_gcd_one'` 📖	—	—	—	—	`exists_gcd_one`
`gcd_def` 📖	—	—	—	—	—
`gcd_div` 📖	—	—	—	—	—
`gcd_div_gcd_div_gcd` 📖	—	—	—	—	—
`gcd_dvd_iff` 📖	—	—	—	—	`gcd_eq_gcd_ab` `mul_assoc`
`gcd_eq_gcd_ab` 📖	mathematical	—	`gcdA` `gcdB`	—	`Nat.gcd_eq_gcd_ab`
`gcd_eq_one_of_gcd_mul_right_eq_one_left` 📖	—	—	—	—	—
`gcd_eq_one_of_gcd_mul_right_eq_one_right` 📖	—	—	—	—	—
`gcd_greatest` 📖	—	—	—	—	—
`gcd_least_linear` 📖	mathematical	—	`IsLeast` `setOf`	—	—
`lcm_def` 📖	—	—	—	—	—
`ne_zero_of_gcd` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₂`

Nat

Definitions

Name	Category	Theorems
`gcdA` 📖	CompOp	9 math math: `gcdA_zero_left`, `Int.gcd_a_modEq`, `CharP.natCast_gcdA_mul_intCast_eq_gcd`, `CharP.intCast_mul_natCast_gcdA_eq_gcd`, `gcdA_zero_right`, `PadicInt.norm_sub_modPart_aux`, `xgcd_val`, `invOf_eq_of_coprime`, `gcd_eq_gcd_ab`
`gcdB` 📖	CompOp	7 math math: `powCoprime_symm_apply`, `gcdB_zero_left`, `nsmulCoprime_symm_apply`, `IsPGroup.powEquiv_symm_apply`, `xgcd_val`, `gcd_eq_gcd_ab`, `gcdB_zero_right`
`xgcd` 📖	CompOp	2 math math: `xgcd_val`, `xgcdAux_val`
`xgcdAux` 📖	CompOp	4 math math: `xgcd_zero_left`, `xgcdAux_rec`, `xgcdAux_val`, `xgcdAux_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mul_emod_eq_gcd` 📖	—	—	—	—	`exists_mul_mod_eq_gcd`
`exists_mul_emod_eq_one_of_coprime` 📖	—	—	—	—	`exists_mul_mod_eq_one_of_coprime`
`exists_mul_mod_eq_gcd` 📖	—	—	—	—	`LT.lt.ne'` `gcd_eq_gcd_ab` `Int.natCast_mod`
`exists_mul_mod_eq_of_coprime` 📖	—	—	—	—	`exists_mul_mod_eq_one_of_coprime` `mul_assoc` `one_mul`
`exists_mul_mod_eq_one_of_coprime` 📖	—	—	—	—	`exists_mul_mod_eq_gcd`
`gcdA_zero_left` 📖	mathematical	—	`gcdA`	—	—
`gcdA_zero_right` 📖	mathematical	—	`gcdA`	—	—
`gcdB_zero_left` 📖	mathematical	—	`gcdB`	—	—
`gcdB_zero_right` 📖	mathematical	—	`gcdB`	—	—
`gcd_eq_gcd_ab` 📖	mathematical	—	`gcdA` `gcdB`	—	`mul_one` `add_zero` `zero_add` `xgcd_val` `xgcdAux_val`
`xgcdAux_fst` 📖	mathematical	—	`xgcdAux`	—	—
`xgcdAux_rec` 📖	mathematical	—	`xgcdAux`	—	`LT.lt.ne'` `xgcdAux.eq_1` `strongRec'_spec`
`xgcdAux_val` 📖	mathematical	—	`xgcdAux` `xgcd`	—	`xgcd.eq_1` `xgcdAux_fst`
`xgcd_val` 📖	mathematical	—	`xgcd` `gcdA` `gcdB`	—	—
`xgcd_zero_left` 📖	mathematical	—	`xgcdAux`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gcd_nsmul_eq_zero` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`mul_nsmul` `nsmul_zero` `IsAddUnit.of_nsmul_eq_zero` `AddUnits.val_nsmul_eq_nsmul_val` `AddUnits.val_zero` `natCast_zsmul` `AddUnits.ext_iff` `Nat.gcd_eq_gcd_ab` `add_zsmul` `mul_zsmul'` `zsmul_zero` `zero_add`
`intGCD_nsmul_eq_zero` 📖	mathematical	—	`AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toZSMul`	—	`gcd_nsmul_eq_zero` `natCast_zsmul` `Int.gcd_ofNat_negSucc` `negSucc_zsmul` `neg_eq_zero` `Int.gcd_negSucc_ofNat` `Int.gcd_negSucc_negSucc`
`nsmul_eq_zero_iff_of_coprime` 📖	mathematical	—	`AddMonoid.toNatSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`gcd_nsmul_eq_zero` `one_nsmul`
`pow_eq_one_iff_of_coprime` 📖	mathematical	—	`Monoid.toNatPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_one`
`pow_eq_pow_iff_of_coprime` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	—	`Commute.pow_eq_pow_iff_of_coprime` `Commute.all`
`pow_gcd_eq_one` 📖	mathematical	—	`Monoid.toNatPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`pow_mul` `one_pow` `IsUnit.of_pow_eq_one` `Units.val_pow_eq_pow_val` `Units.val_one` `zpow_natCast` `Units.ext_iff` `Nat.gcd_eq_gcd_ab` `zpow_add` `zpow_mul` `one_zpow` `one_mul`
`pow_intGCD_eq_one` 📖	mathematical	—	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toZPow`	—	`zpow_natCast` `Int.gcd_ofNat_negSucc` `zpow_negSucc` `Int.gcd_negSucc_ofNat` `Int.gcd_negSucc_negSucc`
`pow_mem_range_pow_of_coprime` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	—	`pow_eq_pow_iff_of_coprime`

---

← Back to Index