Commit 2024-01-09 09:25 7ab8c781

View on Github →

feat: a / b = c / d ↔ a * d = c * b when b, d commute (#9389) This involves moving a bunch of lemmas from Algebra.Group.Units.Hom to Algebra.Group.Units (without modification). From LeanAPAP

Estimated changes

modified theorem Commute.isUnit_mul_iff
modified theorem Commute.units_zpow_left
modified theorem Commute.units_zpow_right
modified def Units.leftOfMul
modified def Units.rightOfMul
modified theorem isUnit_mul_self_iff
added theorem Group.isUnit
added theorem IsUnit.div
added theorem IsUnit.inv
added def IsUnit.unit'
added theorem IsUnit.val_inv_unit'
added theorem divp_eq_div
deleted theorem Group.isUnit
deleted theorem IsUnit.div
deleted theorem IsUnit.inv
deleted def IsUnit.unit'
deleted theorem IsUnit.val_inv_unit'
deleted theorem divp_eq_div