mathlib
1b0a28e1 - chore(*): add mathlib4 synchronization comments (#19055)

Commit
2 years ago
chore(*): add mathlib4 synchronization comments (#19055) 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.projective` * `algebra.monoid_algebra.to_direct_sum` * `analysis.convex.strict_convex_space` * `analysis.convex.uniform` * `analysis.normed_space.banach` * `analysis.normed_space.bounded_linear_maps` * `analysis.normed_space.complemented` * `analysis.normed_space.finite_dimension` * `analysis.normed_space.mazur_ulam` * `analysis.special_functions.log.base` * `analysis.special_functions.log.monotone` * `analysis.special_functions.pow.real` * `combinatorics.additive.salem_spencer` * `data.is_R_or_C.lemmas` * `linear_algebra.adic_completion` * `linear_algebra.cross_product` * `measure_theory.measure.doubling` * `ring_theory.graded_algebra.basic` * `ring_theory.mv_polynomial.homogeneous` * `ring_theory.valuation.extend_to_localization` * `topology.algebra.module.star`
Parents
Loading