Structures · Algebra
IsBezout
A Bézout ring is a ring whose finitely generated ideals are principal.
- Defined in
- Mathlib.RingTheory.PrincipalIdealDomain
- Shape
- One type argument · adds isPrincipal_of_FG
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- Irreducible.coprime_iff_not_dvd
- gcd_isUnit_iff
- isCoprime_of_dvd
- Prime.coprime_iff_not_dvd
- span_gcd
- exists_associated_pow_of_mul_eq_pow'
- IsBezout.isPrincipal_of_FG
- dvd_or_isCoprime
- IsBezout.TFAE
- Module.Flat.flat_iff_torsion_eq_bot_of_isBezout
- Finset.gcd_eq_sum_mul
- gcd_dvd_iff_exists
- Polynomial.isPrimitive_iff_contentIdeal_eq_top
- Irreducible.dvd_iff_not_isCoprime
- IsBezout.span_gcd_eq_span_gcd
- IsBezout.toGCDDomain
- Irreducible.isCoprime_or_dvd
- IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout
- IsBezout.span_pair_isPrincipal
- exists_gcd_eq_mul_add_mul
- exists_associated_pow_of_associated_pow_mul
- Function.Surjective.isBezout
- IsBezout.instIsGCDMonoidOfIsCancelMulZero
- ValuationRing.instOfIsLocalRingOfIsBezout
- Irreducible.coprime_pow_of_not_dvd
Ancestors0
No ancestors.