Commit 2024-08-26 09:52 dee9f4f7

View on Github →

feat: a / b * (c / a) = c / b for CommGroupWithZero (#16111) Moves:

  • div_mul_div_cancel → div_mul_div_cancel₀
  • div_mul_div_cancel' → div_mul_div_cancel
  • div_mul_div_cancel'' → div_mul_div_cancel'
  • div_div_div_cancel_right → div_div_div_cancel_right₀
  • div_div_div_cancel_right' → div_div_div_cancel_right Add the missing div_mul_div_cancel₀'.

Estimated changes

deleted theorem div_div_div_cancel_right'
deleted theorem div_mul_div_cancel''
modified theorem div_mul_div_cancel'
added theorem div_mul_div_cancel
deleted theorem div_div_div_cancel_right
deleted theorem div_mul_div_cancel
added theorem div_mul_div_cancel₀'
added theorem div_mul_div_cancel₀