Commit 2022-12-14 10:06 9f9bb0e8

View on Github →

chore: tidy up some files (#1009)

Estimated changes

Modified Mathlib/Algebra/Divisibility/Basic.lean

Modified Mathlib/Algebra/Group/WithOne/Basic.lean

modified def WithOne.lift

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

added theorem MulEquiv.coe_toMonoidHom

deleted theorem MulEquiv.coe_to_monoidHom

added theorem MulEquiv.toMonoidHom_injective

deleted theorem MulEquiv.to_monoidHom_injective

Modified Mathlib/Algebra/Invertible.lean

added theorem mul_mul_invOf_self_cancel

deleted theorem mul_mul_inv_of_self_cancel

Modified Mathlib/Algebra/Order/Monoid/WithZero/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Defs.lean

added theorem Monotone.mul_strictMono

deleted theorem Monotone.mul_strict_mono

added theorem strictAnti_mul_left

added theorem strictAnti_mul_right

added theorem strictMonoOn_mul_self

added theorem strictMono_mul_left_of_pos

added theorem strictMono_mul_right_of_pos

deleted theorem strict_anti_mul_left

deleted theorem strict_anti_mul_right

deleted theorem strict_mono_mul_left_of_pos

deleted theorem strict_mono_mul_right_of_pos

deleted theorem strict_mono_on_mul_self

Modified Mathlib/Data/List/Defs.lean

Modified Mathlib/Data/Nat/Order/Basic.lean

Modified Mathlib/Data/PSigma/Order.lean

Modified Mathlib/GroupTheory/GroupAction/Units.lean

added theorem Units.smul_isUnit

deleted theorem Units.smul_is_unit

Modified Mathlib/Order/Antisymmetrization.lean

added theorem OrderIso.dualAntisymmetrization_symm_apply

deleted theorem OrderIso.dual_antisymmetrization_symm_apply

added theorem antisymmRel_iff_eq

deleted theorem antisymm_rel_iff_eq

added theorem toAntisymmetrization_ofAntisymmetrization

deleted theorem to_antisymmetrization_of_antisymmetrization

added theorem wellFounded_antisymmetrization_iff

deleted theorem well_founded_antisymmetrization_iff

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/Hom/Basic.lean

added theorem OrderEmbedding.ltEmbedding_apply

deleted theorem OrderEmbedding.lt_embedding_apply

modified def OrderEmbedding.toOrderHom

modified def OrderHom.const

modified def OrderHom.curry

modified def OrderHom.dualIso

added theorem OrderHom.orderHom_eq_id

deleted theorem OrderHom.order_hom_eq_id

modified def OrderHom.piIso

modified def OrderHom.prodIso

modified def OrderIso.funUnique

added theorem RelEmbedding.orderEmbeddingOfLtEmbedding_apply

deleted theorem RelEmbedding.order_embedding_of_lt_embedding_apply

Modified Mathlib/Order/SymmDiff.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean