mathlib
33c67ae6 - chore(*): add mathlib4 synchronization comments (#19042)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19042) Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.category.Mon.limits` * `algebra.char_p.local_ring` * `algebra.direct_sum.decomposition` * `algebra.direct_sum.internal` * `algebra.module.bimodule` * `algebraic_topology.fundamental_groupoid.fundamental_group` * `algebraic_topology.fundamental_groupoid.punit` * `analysis.complex.operator_norm` * `analysis.normed_space.affine_isometry` * `analysis.normed_space.banach_steinhaus` * `analysis.normed_space.completion` * `analysis.normed_space.extend` * `analysis.normed_space.multilinear` * `analysis.special_functions.complex.arg` * `analysis.special_functions.complex.log` * `analysis.special_functions.pow.complex` * `category_theory.bicategory.free` * `category_theory.groupoid.free_groupoid` * `category_theory.monoidal.free.coherence` * `category_theory.monoidal.of_chosen_finite_products.basic` * `category_theory.monoidal.types.basic` * `data.matrix.kronecker` * `data.nat.factorial.double_factorial` * `data.polynomial.expand` * `linear_algebra.matrix.is_diag` * `linear_algebra.tensor_product.matrix` * `linear_algebra.unitary_group` * `number_theory.legendre_symbol.mul_character` * `number_theory.multiplicity` * `ring_theory.finite_presentation` * `ring_theory.ideal.local_ring` * `ring_theory.jacobson_ideal` * `ring_theory.localization.at_prime` * `ring_theory.matrix_algebra` * `ring_theory.nakayama` * `set_theory.game.pgame` * `topology.category.TopCommRing` * `topology.fiber_bundle.constructions` * `topology.sheaves.limits` * `topology.sheaves.presheaf` * `topology.sheaves.presheaf_of_functions` * `topology.sheaves.sheaf`
Parents
Loading