Commit 2023-06-03 07:38 9a4c88cd

View on Github →

feat: port RingTheory.Bezout (#4607)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Bezout.lean

added theorem Function.Surjective.isBezout

added theorem IsBezout.TFAE

added theorem IsBezout.dvd_gcd

added theorem IsBezout.gcd_dvd_left

added theorem IsBezout.gcd_dvd_right

added theorem IsBezout.gcd_eq_sum

added theorem IsBezout.iff_span_pair_isPrincipal

added theorem IsBezout.span_gcd