Commit 2023-04-01 19:08 55209140

View on Github →

chore: tidy various files (#3124)

Estimated changes

Modified Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem AddMonoidHom.coe_mulLeft

added theorem AddMonoidHom.coe_mulRight

deleted theorem AddMonoidHom.coe_mul_left

deleted theorem AddMonoidHom.coe_mul_right

modified def AddMonoidHom.mulLeft

modified def AddMonoidHom.mulRight

added theorem AddMonoidHom.mulRight_apply

deleted theorem AddMonoidHom.mul_right_apply

Modified Mathlib/CategoryTheory/Category/ULift.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

Modified Mathlib/Data/Holor.lean

added theorem Holor.slice_unitVec_mul

deleted theorem Holor.slice_unit_vec_mul

added theorem Holor.sum_unitVec_mul_slice

deleted theorem Holor.sum_unit_vec_mul_slice

Modified Mathlib/Data/PFun.lean

added theorem PFun.dom_toSubtype

added theorem PFun.dom_toSubtype_apply_iff

deleted theorem PFun.dom_to_subtype

deleted theorem PFun.dom_to_subtype_apply_iff

added theorem PFun.mem_toSubtype_iff

deleted theorem PFun.mem_to_subtype_iff

added theorem PFun.preimage_asSubtype

deleted theorem PFun.preimage_as_subtype

added theorem PFun.toSubtype_apply

deleted theorem PFun.to_subtype_apply

Modified Mathlib/Data/Polynomial/Degree/Lemmas.lean

added theorem Polynomial.natDegree_C_mul_eq_of_mul_ne_zero

deleted theorem Polynomial.natDegree_c_mul_eq_of_mul_ne_zero

added theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero

deleted theorem Polynomial.natDegree_mul_c_eq_of_mul_ne_zero

Modified Mathlib/Data/Polynomial/Derivative.lean

added theorem Polynomial.eq_C_of_derivative_eq_zero

deleted theorem Polynomial.eq_c_of_derivative_eq_zero

added theorem Polynomial.iterate_derivative_X

deleted theorem Polynomial.iterate_derivative_x

Modified Mathlib/Data/Polynomial/HasseDeriv.lean

Modified Mathlib/Data/Polynomial/Monic.lean

added theorem Polynomial.natDegree_pow_X_add_C

deleted theorem Polynomial.natDegree_pow_X_add_c

Modified Mathlib/Data/Polynomial/Taylor.lean

Modified Mathlib/Deprecated/Subfield.lean

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

Modified Mathlib/LinearAlgebra/Dfinsupp.lean

modified def Dfinsupp.lapply

modified def Dfinsupp.lmk

deleted theorem Submodule.mem_bsupr_iff_exists_dfinsupp

added theorem Submodule.mem_bsupᵢ_iff_exists_dfinsupp

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

added theorem Polynomial.mul_X_add_nat_cast_comp

deleted theorem Polynomial.mul_x_add_nat_cast_comp

added theorem pochhammer_succ_comp_X_add_one

deleted theorem pochhammer_succ_comp_x_add_one

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/Tactic/TFAE.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/Homeomorph.lean

modified def Homeomorph.funUnique

modified def Homeomorph.piFinTwo.{u}

added def Homeomorph.prodPUnit

deleted def Homeomorph.prodPunit

modified def Homeomorph.setCongr

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

added theorem AntilipschitzWith.to_rightInvOn'

deleted theorem AntilipschitzWith.to_right_inv_on'

Modified Mathlib/Topology/MetricSpace/Infsep.lean