Theorems · Definition · commutative algebra
IsBezout.gcd
{R : Type u} → [inst : Ring R] → (x y : R) → [Submodule.IsPrincipal (Ideal.span {x, y})] → RA choice of gcd of two elements in a Bézout domain. Note that the choice is usually not unique.
- Defined in
- Mathlib.RingTheory.PrincipalIdealDomain
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RingSubmodule.IsPrincipal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Ringstatement and proof · cited by 7,463
- Ideal.spanstatement and proof · cited by 948
- Submodule.IsPrincipalstatement and proof · cited by 129
- Submodule.IsPrincipal.generatorproof · cited by 56
Cited by13
Results whose statement or proof uses this declaration.
- IsRelPrime.isCoprimeproof · cited by 5
- IsBezout.span_gcdstatement · cited by 5
- IsBezout.gcd_dvd_leftstatement · cited by 3
- IsBezout.gcd_dvd_rightstatement · cited by 3
- span_gcdproof · cited by 2
- IsBezout.dvd_gcdstatement · cited by 2
- Finset.gcd_eq_sum_mulproof · cited by 1
- IsBezout.associated_gcd_gcdstatement · cited by 1
- IsBezout.gcd_eq_sumstatement and proof · cited by 1
- IsBezout.span_gcd_eq_span_gcdstatement · cited by 1
- IsBezout.toGCDDomainproof · cited by 1
- IsBezout.gcd.congr_simpstatement and proof · cited by 0