Documentation Verification Report

GCD

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

Statistics

Metric	Count
Definitions `evalIntGCD`, `evalIntLCM`, `evalNatGCD`, `evalNatLCM`, `evalRatDen`, `evalRatNum`, `proveIntGCD`, `proveIntLCM`, `proveNatGCD`, `proveNatLCM`	10
Theorems `int_gcd_helper`, `int_gcd_helper'`, `int_lcm_helper`, `isInt_gcd`, `isInt_lcm`, `isInt_ratNum`, `isNat_gcd`, `isNat_lcm`, `isNat_ratDen`, `nat_gcd_helper_1`, `nat_gcd_helper_1'`, `nat_gcd_helper_2`, `nat_gcd_helper_2'`, `nat_gcd_helper_dvd_left`, `nat_gcd_helper_dvd_right`, `nat_lcm_helper`	16
Total	26

Tactic.NormNum

Definitions

Name	Category	Theorems
`evalIntGCD` 📖	CompOp	—
`evalIntLCM` 📖	CompOp	—
`evalNatGCD` 📖	CompOp	—
`evalNatLCM` 📖	CompOp	—
`evalRatDen` 📖	CompOp	—
`evalRatNum` 📖	CompOp	—
`proveIntGCD` 📖	CompOp	—
`proveIntLCM` 📖	CompOp	—
`proveNatGCD` 📖	CompOp	—
`proveNatLCM` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`int_gcd_helper` 📖	—	—	—	—	`Int.gcd_def`
`int_gcd_helper'` 📖	—	—	—	—	`dvd_add` `Distrib.leftDistribClass` `Dvd.dvd.mul_right`
`int_lcm_helper` 📖	—	—	—	—	`Int.lcm_def`
`isInt_gcd` 📖	mathematical	`Mathlib.Meta.NormNum.IsInt` `Int.instRing`	`Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne`	—	—
`isInt_lcm` 📖	mathematical	`Mathlib.Meta.NormNum.IsInt` `Int.instRing`	`Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne`	—	—
`isInt_ratNum` 📖	mathematical	`Mathlib.Meta.NormNum.IsRat` `DivisionRing.toRing` `Rat.instDivisionRing`	`Mathlib.Meta.NormNum.IsInt` `Int.instRing`	—	`Rat.instCharZero` `Invertible.ne_zero` `Rat.nontrivial` `Rat.mul_num` `invOf_eq_inv` `Rat.inv_natCast_den_of_pos` `Rat.inv_natCast_num_of_pos` `one_mul` `mul_one` `Nat.cast_one`
`isNat_gcd` 📖	—	`Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_lcm` 📖	—	`Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_ratDen` 📖	mathematical	`Mathlib.Meta.NormNum.IsRat` `DivisionRing.toRing` `Rat.instDivisionRing`	`Mathlib.Meta.NormNum.IsNat` `Nat.instAddMonoidWithOne`	—	`Rat.instCharZero` `Invertible.ne_zero` `Rat.nontrivial` `Rat.mul_den` `invOf_eq_inv` `Rat.inv_natCast_den_of_pos` `Rat.inv_natCast_num_of_pos` `one_mul` `mul_one`
`nat_gcd_helper_1` 📖	—	—	—	—	`nat_gcd_helper_2`
`nat_gcd_helper_1'` 📖	—	—	—	—	`nat_gcd_helper_1`
`nat_gcd_helper_2` 📖	—	—	—	—	`int_gcd_helper'` `mul_neg` `sub_eq_add_neg` `sub_eq_iff_eq_add'` `Int.instCharZero`
`nat_gcd_helper_2'` 📖	—	—	—	—	`nat_gcd_helper_2`
`nat_gcd_helper_dvd_left` 📖	—	—	—	—	—
`nat_gcd_helper_dvd_right` 📖	—	—	—	—	—
`nat_lcm_helper` 📖	—	—	—	—	`mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero`

---

← Back to Index