mathlib3

327c3c0d - chore(*): add mathlib4 synchronization comments (#18218)

chore(*): add mathlib4 synchronization comments (#18218) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.big_operators.basic` * `algebra.big_operators.nat_antidiagonal` * `algebra.big_operators.option` * `algebra.big_operators.order` * `algebra.big_operators.pi` * `algebra.big_operators.ring` * `algebra.big_operators.ring_equiv` * `algebra.char_zero.infinite` * `algebra.group.conj_finite` * `algebra.indicator_function` * `algebra.module.big_operators` * `algebra.module.linear_map` * `algebra.order.field.pi` * `algebra.star.big_operators` * `algebra.support` * `combinatorics.additive.energy` * `combinatorics.double_counting` * `combinatorics.quiver.single_obj` * `control.traversable.instances` * `data.W.basic` * `data.finite.basic` * `data.finite.set` * `data.finset.noncomm_prod` * `data.finset.preimage` * `data.finset.sort` * `data.fintype.big_operators` * `data.fintype.card` * `data.fintype.lattice` * `data.fintype.option` * `data.fintype.parity` * `data.fintype.powerset` * `data.fintype.prod` * `data.fintype.small` * `data.fintype.sort` * `data.fintype.sum` * `data.fintype.units` * `data.fintype.vector` * `data.list.fin_range` * `data.list.nodup_equiv_fin` * `data.list.sort` * `data.multiset.sort` * `data.nat.factorial.big_operators` * `data.nat.factors` * `data.nat.fib` * `data.nat.gcd.big_operators` * `data.nat.lattice` * `data.nat.prime_fin` * `data.prod.tprod` * `data.rat.big_operators` * `data.set.finite` * `data.set.pointwise.big_operators` * `data.set.pointwise.list_of_fn` * `data.sym.basic` * `data.vector.basic` * `data.vector.mem` * `group_theory.group_action.big_operators` * `group_theory.submonoid.membership` * `logic.denumerable` * `logic.equiv.list` * `logic.small.list` * `number_theory.frobenius_number` * `order.atoms.finite` * `order.conditionally_complete_lattice.finset` * `order.omega_complete_partial_order` * `ring_theory.coprime.lemmas` * `ring_theory.fintype` * `ring_theory.non_zero_divisors` * `ring_theory.prime`