Commit 2023-05-22 05:47 4280f5f3

View on Github →

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

  • algebra.category.Group.limits
  • algebra.category.Module.kernels
  • algebra.category.Mon.filtered_colimits
  • algebra.char_p.mixed_char_zero
  • algebraic_geometry.presheafed_space
  • algebraic_geometry.projective_spectrum.topology
  • analysis.calculus.fderiv.basic
  • analysis.normed_space.star.mul
  • analysis.special_functions.complex.circle
  • analysis.special_functions.pow.nnreal
  • linear_algebra.matrix.charpoly.basic
  • linear_algebra.matrix.charpoly.coeff
  • linear_algebra.matrix.charpoly.linear_map
  • measure_theory.constructions.borel_space.basic
  • measure_theory.constructions.borel_space.complex
  • measure_theory.constructions.borel_space.continuous_linear_map
  • measure_theory.constructions.polish
  • measure_theory.function.ae_measurable_order
  • measure_theory.function.ess_sup
  • measure_theory.function.floor
  • measure_theory.function.simple_func
  • measure_theory.function.simple_func_dense
  • measure_theory.function.special_functions.basic
  • measure_theory.integral.lebesgue
  • measure_theory.measure.regular
  • measure_theory.measure.stieltjes
  • number_theory.class_number.admissible_card_pow_degree
  • ring_theory.graded_algebra.homogeneous_ideal
  • ring_theory.graded_algebra.homogeneous_localization
  • ring_theory.ideal.minimal_prime
  • ring_theory.polynomial_algebra
  • topology.algebra.module.locally_convex
  • topology.continuous_function.bounded
  • topology.sheaves.sheaf_condition.sites

Estimated changes