Commit 2025-01-07 20:33 97a203a2

View on Github →

chore: move results about DivisionMonoid + HasDistribNeg (#20551) This way, we don't have to import fields to use those lemmas

Estimated changes

deleted theorem div_neg
deleted theorem div_neg_eq_neg_div
deleted theorem inv_neg
deleted theorem inv_neg_one
deleted theorem neg_div'
deleted theorem neg_div
deleted theorem neg_div_neg_eq
deleted theorem neg_inv
added theorem div_neg
added theorem div_neg_eq_neg_div
added theorem inv_neg
added theorem inv_neg_one
added theorem neg_div'
added theorem neg_div
added theorem neg_div_neg_eq
added theorem neg_inv