Theorems · Theorem · number theory
PNat.gcd_eq
∀ (a b : ℕ+), a.gcdD b = a.gcd b
- Defined in
- Mathlib.Data.PNat.Xgcd
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_commproof · cited by 2,262
- PNatstatement and proof · cited by 392
- PNat.valproof · cited by 226
- Dvd.dvd.transproof · cited by 148
- dvd_mul_leftproof · cited by 47
- Nat.succPNatproof · cited by 29
- PNat.gcdstatement and proof · cited by 27
- Dvd.introproof · cited by 26
- PNat.dvd_iffproof · cited by 13
- PNat.gcd_propsproof · cited by 8
- PNat.gcdA'proof · cited by 6
- PNat.gcdB'proof · cited by 6
Cited by4
Results whose statement or proof uses this declaration.
- PNat.gcd_a_eqproof · cited by 0
- PNat.gcd_b_eqproof · cited by 0
- PNat.gcd_rel_leftproof · cited by 0
- PNat.gcd_rel_rightproof · cited by 0