Commit 2023-09-11 18:53 5cffe216

View on Github →

chore: split Algebra.Semiconj and Algebra.Commute (#7098)

Estimated changes

added theorem Commute.inv_inv_iff
deleted theorem Commute.inv_inv_iff
deleted theorem Commute.inv_left
deleted theorem Commute.inv_left_iff
deleted theorem Commute.inv_right
deleted theorem Commute.inv_right_iff
deleted theorem Commute.isUnit_mul_iff
deleted theorem Commute.units_inv_left
deleted theorem Commute.units_inv_right
deleted theorem Commute.units_of_val
deleted theorem Commute.units_val
deleted theorem Commute.units_val_iff
deleted def Units.leftOfMul
deleted def Units.rightOfMul
deleted theorem inv_mul_cancel_comm
deleted theorem inv_mul_cancel_comm_assoc
deleted theorem isUnit_mul_self_iff
added theorem Commute.inv_left
added theorem Commute.inv_left_iff
added theorem Commute.inv_right
added theorem Commute.inv_right_iff
added theorem Commute.isUnit_mul_iff
added theorem Commute.units_inv_left
added theorem Commute.units_of_val
added theorem Commute.units_val
added theorem Commute.units_val_iff
added def Units.leftOfMul
added def Units.rightOfMul
added theorem inv_mul_cancel_comm
added theorem isUnit_mul_self_iff
deleted theorem SemiconjBy.inv_inv_symm
deleted theorem SemiconjBy.inv_right
deleted theorem SemiconjBy.inv_right_iff
deleted theorem SemiconjBy.inv_symm_left
deleted theorem SemiconjBy.units_of_val
deleted theorem SemiconjBy.units_val
deleted theorem SemiconjBy.units_val_iff
deleted theorem Units.mk_semiconjBy
added theorem SemiconjBy.inv_right
added theorem SemiconjBy.units_val
added theorem Units.mk_semiconjBy