Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 21:40 b0cd1f9c

View on Github →

chore(algebra/group): move is_unit.inv lemmas (#9364)

Estimated changes

Modified src/algebra/group/units.lean

added theorem is_unit.coe_inv_mul

added theorem is_unit.mul_coe_inv

Modified src/group_theory/group_action/units.lean

added theorem is_unit.inv_smul

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

deleted theorem is_unit.coe_inv_mul

deleted theorem is_unit.inv_smul

deleted theorem is_unit.mul_coe_inv