Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-07-12 21:43
3543262a
View on Github →
feat(ring_theory/bezout): Define Bézout rings. (
#15091
)
Estimated changes
Created
src/ring_theory/bezout.lean
added
theorem
function.surjective.is_bezout
added
theorem
is_bezout.dvd_gcd
added
def
is_bezout.gcd
added
theorem
is_bezout.gcd_dvd_left
added
theorem
is_bezout.gcd_dvd_right
added
theorem
is_bezout.gcd_eq_sum
added
theorem
is_bezout.iff_span_pair_is_principal
added
theorem
is_bezout.span_gcd
added
theorem
is_bezout.tfae
added
def
is_bezout.to_gcd_domain
Modified
src/ring_theory/noetherian.lean
added
theorem
is_noetherian_iff_fg_well_founded
added
theorem
submodule.fg_induction