mathlib3
19cb3751 - chore(*): add mathlib4 synchronization comments (#18753)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#18753) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_topology.simplex_category` * `analysis.hofer` * `analysis.normed.group.pointwise` * `analysis.specific_limits.basic` * `category_theory.idempotents.basic` * `category_theory.idempotents.functor_categories` * `category_theory.idempotents.functor_extension` * `category_theory.idempotents.karoubi` * `category_theory.idempotents.karoubi_karoubi` * `data.matrix.pequiv` * `data.nat.choose.multinomial` * `group_theory.perm.fin` * `linear_algebra.affine_space.combination` * `linear_algebra.finsupp_vector_space` * `linear_algebra.free_module.basic` * `linear_algebra.matrix.dot_product` * `linear_algebra.multilinear.basic` * `linear_algebra.multilinear.basis` * `linear_algebra.multilinear.tensor_product` * `linear_algebra.std_basis` * `linear_algebra.tensor_product_basis` * `ring_theory.mv_polynomial.basic` * `ring_theory.quotient_nilpotent` * `ring_theory.quotient_noetherian` * `ring_theory.simple_module` * `ring_theory.valuation.quotient` * `set_theory.zfc.basic` * `topology.algebra.filter_basis` * `topology.algebra.module.linear_pmap` * `topology.algebra.module.simple` * `topology.algebra.star_subalgebra` * `topology.algebra.uniform_field` * `topology.algebra.uniform_filter_basis` * `topology.metric_space.hausdorff_distance`
Parents
Loading