Theorems · Definition · number theory
PNat.gcdX
ℕ+ → ℕ+ → ℕ
Final value of x
- Defined in
- Mathlib.Data.PNat.Xgcd
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PNatstatement and proof · cited by 392
- PNat.XgcdType.xproof · cited by 11
- PNat.xgcdproof · cited by 2
Cited by6
Results whose statement or proof uses this declaration.
- PNat.gcd_propsstatement and proof · cited by 8
- PNat.gcd_eqproof · cited by 4
- PNat.gcdA'_coestatement · cited by 1
- PNat.gcd_det_eqstatement · cited by 0
- PNat.gcd_rel_leftstatement · cited by 0
- PNat.gcd_rel_left'statement · cited by 0