Commit 2023-05-24 04:13 61db041a

View on Github →

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

  • algebra.category.Ring.colimits
  • analysis.box_integral.partition.additive
  • analysis.calculus.formal_multilinear_series
  • analysis.convex.cone.basic
  • analysis.convex.side
  • data.nat.prime_norm_num
  • field_theory.ax_grothendieck
  • field_theory.intermediate_field
  • field_theory.separable
  • linear_algebra.annihilating_polynomial
  • linear_algebra.charpoly.basic
  • linear_algebra.free_module.strong_rank_condition
  • linear_algebra.matrix.charpoly.minpoly
  • linear_algebra.matrix.special_linear_group
  • linear_algebra.trace
  • measure_theory.function.strongly_measurable.basic
  • representation_theory.basic
  • ring_theory.fractional_ideal
  • ring_theory.hahn_series
  • ring_theory.henselian
  • ring_theory.ideal.over
  • ring_theory.localization.integral
  • ring_theory.power_basis
  • topology.instances.irrational
  • topology.sheaves.sheaf_condition.opens_le_cover

Estimated changes