Commit 2024-04-27 06:15 ea608559

View on Github →

feat: Axiomatise b ≠ 0 → a * b / b = a (#12424) This lets us unify a few lemmas between GroupWithZero and EuclideanDomain and two lemmas that were previously proved separately for Nat, Int, Polynomial.

Estimated changes

modified theorem Semifield.toIsField
deleted theorem Finset.Int.gcd_div_eq_one
deleted theorem Finset.Nat.gcd_div_eq_one
added theorem Finset.gcd_div_eq_one
added theorem mul_div_cancel_left₀
modified theorem mul_inv_cancel
deleted theorem mul_div_cancel_left₀
deleted theorem mul_div_cancel_right₀