mathlib
ce38d86c - chore(*): add mathlib4 synchronization comments (#18813)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#18813) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.homology.homological_complex` * `algebra.homology.image_to_kernel` * `algebraic_topology.Moore_complex` * `algebraic_topology.topological_simplex` * `analysis.asymptotics.asymptotic_equivalent` * `analysis.box_integral.box.subbox_induction` * `analysis.convex.body` * `analysis.convex.exposed` * `analysis.normed.group.add_torsor` * `analysis.normed.ring.seminorm` * `analysis.normed_space.add_torsor` * `analysis.normed_space.pointwise` * `analysis.special_functions.polynomials` * `category_theory.sites.whiskering` * `category_theory.subobject.basic` * `category_theory.subobject.factor_thru` * `category_theory.subobject.lattice` * `category_theory.subobject.limits` * `category_theory.subobject.mono_over` * `category_theory.subobject.well_powered` * `data.num.prime` * `dynamics.circle.rotation_number.translation_number` * `geometry.manifold.local_invariant_properties` * `group_theory.free_abelian_group_finsupp` * `linear_algebra.free_module.finite.rank` * `model_theory.syntax` * `number_theory.lucas_lehmer` * `number_theory.pell_matiyasevic` * `order.category.DistLat` * `ring_theory.non_unital_subsemiring.basic` * `topology.algebra.nonarchimedean.bases` * `topology.metric_space.baire` * `topology.metric_space.closeds`
Parents
Loading