Commit 2022-12-21 11:12 2a588a7d

View on Github →

chore: tidy various files (#1145)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

deleted theorem Int.abs_le_self_sq

added theorem Int.natAbs_le_self_sq

added theorem Int.natAbs_pow

added theorem Int.natAbs_sq'

added theorem Int.natAbs_sq

deleted theorem Int.nat_abs_pow

deleted theorem Int.nat_abs_sq'

deleted theorem Int.nat_abs_sq

added theorem Units.pow_ofPowEqOne

deleted theorem Units.pow_of_pow_eq_one

added theorem invOf_pow

deleted theorem inv_of_pow

added theorem isUnit_ofPowEqOne

added theorem isUnit_pow_iff

added theorem isUnit_pow_succ_iff

deleted theorem is_unit_of_pow_eq_one

deleted theorem is_unit_pow_iff

deleted theorem is_unit_pow_succ_iff

added theorem multiplesAddHom_symm_apply

modified def multiplesHom

added theorem multiplesHom_apply

added theorem multiplesHom_symm_apply

deleted theorem multiples_add_hom_symm_apply

deleted theorem multiples_hom_apply

deleted theorem multiples_hom_symm_apply

modified def powersHom

added theorem powersHom_apply

added theorem powersHom_symm_apply

added theorem powersMulHom_apply

added theorem powersMulHom_symm_apply

deleted theorem powers_hom_apply

deleted theorem powers_hom_symm_apply

deleted theorem powers_mul_hom_apply

deleted theorem powers_mul_hom_symm_apply

added theorem strictMono_pow_bit1

deleted theorem strict_mono_pow_bit1

added theorem zmultiplesAddHom_apply

added theorem zmultiplesAddHom_symm_apply

added theorem zmultiplesHom_apply

added theorem zmultiplesHom_symm_apply

deleted theorem zmultiples_add_hom_apply

deleted theorem zmultiples_add_hom_symm_apply

deleted theorem zmultiples_hom_apply

deleted theorem zmultiples_hom_symm_apply

added theorem zpow_strictMono_left

added theorem zpow_strictMono_right

deleted theorem zpow_strict_mono_left

deleted theorem zpow_strict_mono_right

added theorem zpowersHom_apply

added theorem zpowersHom_symm_apply

added theorem zpowersMulHom_apply

added theorem zpowersMulHom_symm_apply

deleted theorem zpowers_hom_apply

deleted theorem zpowers_hom_symm_apply

deleted theorem zpowers_mul_hom_apply

deleted theorem zpowers_mul_hom_symm_apply

Modified Mathlib/Algebra/Parity.lean

added theorem Odd.strictMono_pow

deleted theorem Odd.strict_mono_pow

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/Data/Erased.lean

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

added theorem Function.Semiconj.mapsTo_fixedPoints

deleted theorem Function.Semiconj.maps_to_fixedPoints

added theorem Function.mapsTo_fixedPoints_comp

deleted theorem Function.maps_to_fixedPoints_comp

Modified Mathlib/GroupTheory/GroupAction/Opposite.lean

Modified Mathlib/GroupTheory/GroupAction/Pi.lean

Modified Mathlib/Order/CompleteLattice.lean

added theorem ofDual_infᵢ

added theorem ofDual_infₛ

added theorem ofDual_supᵢ

added theorem ofDual_supₛ

deleted theorem of_dual_infᵢ

deleted theorem of_dual_infₛ

deleted theorem of_dual_supᵢ

deleted theorem of_dual_supₛ

added theorem toDual_infᵢ

added theorem toDual_infₛ

added theorem toDual_supᵢ

added theorem toDual_supₛ

deleted theorem to_dual_infᵢ

deleted theorem to_dual_infₛ

deleted theorem to_dual_supᵢ

deleted theorem to_dual_supₛ

Modified Mathlib/Order/GaloisConnection.lean

added theorem GaloisCoinsertion.strictMono_l

deleted theorem GaloisCoinsertion.strict_mono_l

added theorem GaloisInsertion.strictMono_u

deleted theorem GaloisInsertion.strict_mono_u

added theorem Nat.galoisConnection_mul_div

deleted theorem Nat.galois_connection_mul_div

Modified Mathlib/Order/Hom/Set.lean