Commit 2023-05-21 06:27 1b0a28e1

View on Github →

chore(*): add mathlib4 synchronization comments (#19055) Regenerated from the port status wiki page. 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

Estimated changes