Commit 2024-05-25 14:09 c92909de

View on Github →

chore: Do not import MonoidWithZero in Data.Rat.Defs (#13138) Move the Ring and GroupWithZero instances to a new file Algebra.Ring.Rat.

Estimated changes

deleted theorem Int.natAbs_pow
added theorem Rat.den_mul_eq_num
added theorem Rat.divInt_pow
added theorem Rat.mkRat_eq_div
added theorem Rat.mkRat_pow
added theorem Rat.mul_den_eq_num
added theorem Rat.natCast_eq_divInt
added theorem Rat.num_div_den
added theorem Int.natAbs_pow
deleted theorem Rat.den_mul_eq_num
deleted theorem Rat.divInt_pow
deleted theorem Rat.mkRat_eq_div
deleted theorem Rat.mkRat_pow
deleted theorem Rat.mul_den_eq_num
deleted theorem Rat.natCast_eq_divInt
deleted theorem Rat.num_div_den