Commit 2024-01-06 09:51 7522333a

View on Github →

Chore: Move Units lemmas earlier (#9461) Part of #9411

Estimated changes

Modified Mathlib/Algebra/Group/Commute/Units.lean

added theorem Commute.units_zpow_left

added theorem Commute.units_zpow_right

added def Units.ofPow

added def Units.ofPowEqOne

added theorem Units.pow_ofPowEqOne

added theorem isUnit_ofPowEqOne

added theorem isUnit_pow_iff

added theorem isUnit_pow_succ_iff

Modified Mathlib/Algebra/Group/Semiconj/Units.lean

added theorem SemiconjBy.units_zpow_right

added theorem Units.conj_pow'

added theorem Units.conj_pow

modified theorem Units.mk_semiconjBy

Modified Mathlib/Algebra/Group/Units.lean

modified theorem IsUnit.exists_left_inv

modified theorem IsUnit.exists_right_inv

modified theorem IsUnit.mul

added theorem IsUnit.pow

added theorem Units.commute_coe_inv

added theorem Units.commute_inv_coe

added theorem Units.val_div_eq_div_val

modified theorem Units.val_inv_eq_inv_val

added theorem Units.val_pow_eq_pow_val

Modified Mathlib/Algebra/Group/Units/Hom.lean

deleted theorem Units.val_div_eq_div_val

deleted theorem Units.val_pow_eq_pow_val

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

deleted theorem Commute.units_zpow_left

deleted theorem Commute.units_zpow_right

deleted theorem IsUnit.pow

deleted theorem SemiconjBy.units_zpow_right

deleted theorem Units.conj_pow'

deleted theorem Units.conj_pow

deleted def Units.ofPow

deleted def Units.ofPowEqOne

deleted theorem Units.pow_ofPowEqOne

deleted theorem invOf_pow

deleted def invertibleOfPowEqOne

deleted theorem isUnit_ofPowEqOne

deleted theorem isUnit_pow_iff

deleted theorem isUnit_pow_succ_iff

Modified Mathlib/Algebra/Invertible/Basic.lean

added theorem invOf_pow

added def invertibleOfPowEqOne

Modified Mathlib/GroupTheory/GroupAction/Units.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

Modified test/instance_diamonds.lean