Bezout

📁 Source: Mathlib/RingTheory/Bezout.lean

Statistics

Metric	Count
Definitions	0
Theorems isBezout, iff_span_pair_isPrincipal	2
Total	2

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBezout 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsBezout	—	IsBezout.iff_span_pair_isPrincipal IsBezout.span_pair_isPrincipal IsBezout.span_gcd Ideal.map_span RingHom.instRingHomClass Set.image_insert_eq Set.image_singleton

IsBezout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_span_pair_isPrincipal 📖	mathematical	—	IsBezout CommSemiring.toSemiring CommRing.toCommSemiring Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instInsert Set.instSingletonSet	—	span_pair_isPrincipal Submodule.fg_induction Submodule.span_insert

---

← Back to Index