Commit 2023-02-06 06:28 0a0ec350
View on Github →chore(*): add mathlib4 synchronization comments (#18387) Regenerated from the port status wiki page. Relates to the following files:
combinatorics.colex
combinatorics.set_family.harris_kleitman
data.finset.pimage
data.fintype.perm
data.holor
dynamics.minimal
order.filter.partial
order.partition.equipartition
order.partition.finpartition
topology.extend_from
topology.order.basic
topology.paracompact
topology.shrinking_lemma
topology.uniform_space.absolute_value
topology.uniform_space.complete_separated
topology.uniform_space.pi
topology.uniform_space.uniform_convergence
topology.uniform_space.uniform_embedding