Commit 2024-10-14 13:31 a67c43d5

View on Github →

chore(Algebra.Group.Units): split into Defs and Basic file (#17724) The criteria for including a result in Algebra.Group.Unit.Defs:

  • Can it be defined with only Defs imports?
  • Is it needed for a subsequent def or instance?

Estimated changes

added theorem IsUnit.mul_left_inj
added theorem IsUnit.mul_right_inj
added theorem Units.inv_mul_eq_one
added theorem Units.inv_unique
added theorem Units.mul_inv_eq_one
added theorem Units.mul_left_inj
added theorem Units.mul_right_inj
added theorem divp_eq_divp_iff
added theorem divp_eq_iff_mul_eq
added theorem divp_eq_one_iff_eq
added theorem divp_left_inj
added theorem divp_mul_divp
added theorem divp_mul_eq_mul_divp
added theorem eq_divp_iff_mul_eq
added theorem eq_one_of_mul_left'
added theorem eq_one_of_mul_left
added theorem eq_one_of_mul_right'
added theorem eq_one_of_mul_right
added theorem inv_eq_one_divp'
added theorem isUnit_of_subsingleton
added theorem mul_eq_one'
added theorem mul_eq_one
added theorem mul_ne_one'
added theorem mul_ne_one
added theorem unique_one
added theorem units_eq_one
deleted theorem IsUnit.mul_left_inj
deleted theorem IsUnit.mul_right_inj
deleted theorem Units.inv_mul_eq_one
deleted theorem Units.inv_unique
deleted theorem Units.mul_inv_eq_one
deleted theorem Units.mul_left_inj
deleted theorem Units.mul_right_inj
deleted theorem divp_eq_divp_iff
deleted theorem divp_eq_iff_mul_eq
deleted theorem divp_eq_one_iff_eq
deleted theorem divp_left_inj
deleted theorem divp_mul_divp
deleted theorem divp_mul_eq_mul_divp
deleted theorem eq_divp_iff_mul_eq
deleted theorem eq_one_of_mul_left'
deleted theorem eq_one_of_mul_left
deleted theorem eq_one_of_mul_right'
deleted theorem eq_one_of_mul_right
deleted theorem inv_eq_one_divp'
deleted theorem isUnit_of_subsingleton
deleted theorem mul_eq_one'
deleted theorem mul_eq_one
deleted theorem mul_ne_one'
deleted theorem mul_ne_one
deleted theorem unique_one
deleted theorem units_eq_one