Commit 2023-05-30 08:50 f60c6087
View on Github →chore(*): add mathlib4 synchronization comments (#19115) Regenerated from the port status wiki page. Relates to the following files:
algebra.category.Group.biproducts
algebra.category.Module.monoidal.basic
algebra.category.Ring.adjunctions
algebra.monoid_algebra.grading
analysis.calculus.deriv.add
analysis.calculus.deriv.basic
analysis.calculus.deriv.comp
analysis.calculus.deriv.inverse
analysis.calculus.deriv.linear
analysis.calculus.deriv.mul
analysis.calculus.deriv.polynomial
analysis.calculus.deriv.pow
analysis.calculus.deriv.prod
analysis.calculus.deriv.slope
analysis.calculus.deriv.star
analysis.calculus.deriv.support
analysis.calculus.fderiv_measurable
analysis.calculus.local_extr
analysis.convex.cone.dual
analysis.inner_product_space.lax_milgram
analysis.inner_product_space.pi_L2
category_theory.bicategory.coherence
category_theory.limits.fubini
category_theory.monoidal.coherence_lemmas
geometry.euclidean.sphere.basic
geometry.euclidean.sphere.power
geometry.euclidean.sphere.second_inter
group_theory.complement
group_theory.sylow
linear_algebra.matrix.hermitian
measure_theory.constructions.prod.basic
measure_theory.function.lp_order
measure_theory.function.lp_seminorm
measure_theory.function.lp_space
measure_theory.measure.complex
measure_theory.measure.vector_measure
number_theory.padics.ring_homs
ring_theory.ideal.cotangent
topology.metric_space.metrizable_uniformity
topology.sheaves.forget
topology.sheaves.sheaf_condition.unique_gluing
topology.sheaves.sheaf_of_functions