mathlib3
9d2f0748 - chore(*): add mathlib4 synchronization comments (#18853)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#18853) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Module.tannaka` * `algebra.homology.homotopy_category` * `algebra.homology.short_exact.preadditive` * `algebraic_topology.dold_kan.equivalence_additive` * `algebraic_topology.dold_kan.functor_gamma` * `algebraic_topology.dold_kan.gamma_comp_n` * `algebraic_topology.dold_kan.homotopy_equivalence` * `algebraic_topology.dold_kan.n_comp_gamma` * `algebraic_topology.dold_kan.normalized` * `analysis.box_integral.partition.basic` * `analysis.box_integral.partition.split` * `analysis.convex.caratheodory` * `analysis.convex.combination` * `analysis.convex.independent` * `analysis.convex.jensen` * `analysis.convex.join` * `analysis.convex.normed` * `analysis.convex.simplicial_complex.basic` * `analysis.convex.topology` * `analysis.locally_convex.bounded` * `analysis.normed_space.conformal_linear_map` * `analysis.normed_space.linear_isometry` * `analysis.normed_space.star.basic` * `analysis.seminorm` * `category_theory.abelian.opposite` * `category_theory.abelian.subobject` * `category_theory.adjunction.adjoint_functor_theorems` * `category_theory.concrete_category.unbundled_hom` * `category_theory.generator` * `category_theory.limits.constructions.weakly_initial` * `category_theory.limits.preserves.functor_category` * `category_theory.limits.presheaf` * `category_theory.limits.shapes.wide_equalizers` * `category_theory.linear.yoneda` * `category_theory.preadditive.generator` * `category_theory.preadditive.yoneda.basic` * `category_theory.subobject.comma` * `data.real.hyperreal` * `data.string.defs` * `linear_algebra.affine_space.basis` * `linear_algebra.finite_dimensional` * `linear_algebra.matrix.absolute_value` * `linear_algebra.matrix.circulant` * `linear_algebra.matrix.nonsingular_inverse` * `linear_algebra.vandermonde` * `topology.extremally_disconnected` * `topology.instances.matrix`
Parents
Loading