Commit 2023-03-17 14:06 f03c405e

View on Github →

chore: tidy various files (#2950)

Estimated changes

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Algebra/Star/Subalgebra.lean

modified def StarSubalgebra.inclusion

Modified Mathlib/Analysis/Normed/Group/Hom.lean

modified def NormedAddGroupHom.coeAddHom

modified def NormedAddGroupHom.incl

modified def NormedAddGroupHom.ker.lift

added theorem NormedAddGroupHom.le_of_opNorm_le

deleted theorem NormedAddGroupHom.le_of_op_norm_le

Modified Mathlib/CategoryTheory/Category/Pointed.lean

modified def Pointed.Iso.mk

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

modified def CategoryTheory.Limits.imageFactorisationZero

Modified Mathlib/CategoryTheory/Monoidal/End.lean

modified def CategoryTheory.endofunctorMonoidalCategory

Modified Mathlib/Combinatorics/Hindman.lean

deleted def Ultrafilter.hasMul

added def Ultrafilter.mul

Modified Mathlib/Data/MvPolynomial/Comap.lean

Modified Mathlib/Data/Polynomial/HasseDeriv.lean

modified theorem Polynomial.hasseDeriv_apply

Modified Mathlib/Data/Polynomial/Lifts.lean

added theorem Polynomial.C_mem_lifts

added theorem Polynomial.X_mem_lifts

added theorem Polynomial.X_pow_mem_lifts

deleted theorem Polynomial.c_mem_lifts

deleted theorem Polynomial.x_mem_lifts

deleted theorem Polynomial.x_pow_mem_lifts

Modified Mathlib/GroupTheory/Commensurable.lean

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

added def Subgroup.equivSMul

deleted def Subgroup.equivSmul

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Subring/Pointwise.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/Instances/NNReal.lean

deleted theorem NNReal.infᵢ_real_pos_eq_infᵢ_nNReal_pos

added theorem NNReal.infᵢ_real_pos_eq_infᵢ_nnreal_pos

Modified Mathlib/Topology/LocallyConstant/Algebra.lean

Modified Mathlib/Topology/MetricSpace/Algebra.lean