mathlib
c416a486 - feat(algebra/gcd_monoid): move the `gcd_monoid nat` instance (#7180)

Commit
4 years ago
feat(algebra/gcd_monoid): move the `gcd_monoid nat` instance (#7180) moves `gcd_monoid nat` instance, removes corresponding todos. removes: * `nat.normalize_eq` -- use `normalize_eq` instead renames: * `nat.gcd_eq_gcd` to `gcd_eq_nat_gcd` * `nat.lcm_eq_lcm` to `lcm_eq_nat_lcm` Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Parents
Loading