Commit 2024-03-23 16:05 4ea4a86a

View on Github →

chore: Rename mul-div cancellation lemmas (#11530) Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the GroupWithZero lemma name, the Group lemma, the AddGroup lemma name). | Statement | New name | Old name | |

Estimated changes

modified theorem half_add_self
deleted theorem div_mul_cancel'''
deleted theorem div_mul_cancel''
deleted theorem div_mul_cancel'
added theorem div_mul_cancel
added theorem div_mul_cancel_left
added theorem div_mul_cancel_right
deleted theorem mul_div_cancel'''
deleted theorem mul_div_cancel''
deleted theorem mul_div_cancel'_right
added theorem mul_div_cancel
added theorem mul_div_cancel_left
added theorem mul_div_cancel_right
deleted theorem div_mul_cancel
added theorem div_mul_cancel_left₀
added theorem div_mul_cancel₀
deleted theorem mul_div_cancel'
deleted theorem mul_div_cancel
deleted theorem mul_div_cancel_left
added theorem mul_div_cancel_left₀
added theorem mul_div_cancel₀
modified theorem lie_lie
modified theorem Complex.cos_sq'
modified theorem Complex.sin_sq
modified theorem Real.cos_sq'
modified theorem Int.cast_div
modified theorem Nat.cast_div