Commit 2023-05-25 02:59 a87d2257

View on Github →

chore(*): add mathlib4 synchronization comments (#19089) Regenerated from the port status wiki page. Relates to the following files:

  • algebra.category.Group.filtered_colimits
  • algebra.category.Module.limits
  • algebra.direct_limit
  • algebraic_geometry.prime_spectrum.basic
  • algebraic_geometry.prime_spectrum.is_open_comap_C
  • analysis.calculus.fderiv.star
  • analysis.complex.isometry
  • analysis.locally_convex.with_seminorms
  • analysis.normed.mul_action
  • analysis.normed_space.hahn_banach.extension
  • data.fintype.quotient
  • field_theory.separable_degree
  • linear_algebra.charpoly.to_matrix
  • linear_algebra.matrix.general_linear_group
  • linear_algebra.matrix.to_linear_equiv
  • measure_theory.function.ae_eq_fun
  • model_theory.quotients
  • number_theory.modular_forms.congruence_subgroups
  • ring_theory.adjoin.power_basis
  • ring_theory.adjoin_root
  • ring_theory.laurent_series
  • topology.instances.rat_lemmas
  • topology.metric_space.gromov_hausdorff_realized

Estimated changes