Commit 2022-12-07 23:03 ad714559

View on Github →

feat: port Algebra.EuclideanDomain.Defs (#871) mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/EuclideanDomain/Defs.lean

added theorem EuclideanDomain.GCD.induction

added theorem EuclideanDomain.div_add_mod'

added theorem EuclideanDomain.div_add_mod

added theorem EuclideanDomain.div_zero

added def EuclideanDomain.gcd

added def EuclideanDomain.gcdA

added theorem EuclideanDomain.gcdA_zero_left

added def EuclideanDomain.gcdB

added theorem EuclideanDomain.gcdB_zero_left

added theorem EuclideanDomain.gcd_zero_left

added def EuclideanDomain.lcm

added theorem EuclideanDomain.lt_one

added theorem EuclideanDomain.mod_add_div'

added theorem EuclideanDomain.mod_add_div

added theorem EuclideanDomain.mod_eq_sub_mul_div

added theorem EuclideanDomain.mod_lt

added theorem EuclideanDomain.mod_zero

added theorem EuclideanDomain.mul_right_not_lt

added theorem EuclideanDomain.val_dvd_le

added def EuclideanDomain.xgcd

added def EuclideanDomain.xgcdAux

added theorem EuclideanDomain.xgcdAux_rec

added theorem EuclideanDomain.xgcd_val

added theorem EuclideanDomain.xgcd_zero_left

Modified scripts/nolints.json