Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-10 13:11 c3f6fce7

View on Github →

feat(algebra/group_power/basic): add lemmas about pow and neg on units (#11447) In future we might want to add a typeclass for monoids with a well-behaved negation operator to avoid needing to repeat these lemmas. Such a typeclass would also apply to the unitary submonoid too.

Estimated changes

Modified src/algebra/group/units_hom.lean

added theorem units.coe_pow

added theorem units.coe_zpow

Modified src/algebra/group_power/basic.lean

added theorem units.eq_or_eq_neg_of_sq_eq_sq

added theorem units.neg_one_pow_eq_or

added theorem units.neg_pow

added theorem units.neg_pow_bit0

added theorem units.neg_pow_bit1

added theorem units.neg_sq

Modified src/algebra/group_power/lemmas.lean

deleted theorem units.coe_pow

deleted theorem units.coe_zpow

Modified src/algebra/ring/basic.lean

added theorem commute.units_neg_left

added theorem commute.units_neg_left_iff

added theorem commute.units_neg_one_left

added theorem commute.units_neg_one_right

added theorem commute.units_neg_right

added theorem commute.units_neg_right_iff

added theorem semiconj_by.units_neg_left

added theorem semiconj_by.units_neg_left_iff

added theorem semiconj_by.units_neg_one_left

added theorem semiconj_by.units_neg_one_right

added theorem semiconj_by.units_neg_right

added theorem semiconj_by.units_neg_right_iff

added theorem units.mul_neg_one

added theorem units.neg_mul_eq_mul_neg

added theorem units.neg_mul_eq_neg_mul

added theorem units.neg_one_mul