Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 18:15 9c3cb72c

View on Github →

feat(data/int/basic): Add unit lemmas (#13565) This PR adds a few more unit lemmas, and cleans up some of the proofs.

Estimated changes

deleted theorem int.units_sq
added theorem int.is_unit_mul_self
added theorem int.is_unit_sq
modified theorem int.units_inv_eq_self
added theorem int.units_sq