Commit 2023-05-23 01:09 38df578a

View on Github →

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

  • algebra.algebraic_card
  • algebra.category.GroupWithZero
  • algebra.category.Ring.instances
  • algebra.dual_quaternion
  • algebra.quaternion
  • algebra.quaternion_basis
  • analysis.calculus.fderiv.add
  • analysis.calculus.fderiv.comp
  • analysis.calculus.fderiv.equiv
  • analysis.calculus.fderiv.linear
  • analysis.calculus.fderiv.prod
  • analysis.calculus.fderiv.restrict_scalars
  • analysis.convex.between
  • analysis.convex.strict_convex_between
  • analysis.locally_convex.strong_topology
  • combinatorics.configuration
  • data.real.irrational
  • dynamics.ergodic.conservative
  • field_theory.minpoly.basic
  • field_theory.minpoly.field
  • group_theory.perm.cycle.concrete
  • linear_algebra.bilinear_form
  • linear_algebra.bilinear_form.tensor_product
  • linear_algebra.coevaluation
  • linear_algebra.contraction
  • linear_algebra.dual
  • linear_algebra.matrix.dual
  • measure_theory.constructions.borel_space.metrizable
  • measure_theory.covering.vitali
  • measure_theory.function.special_functions.is_R_or_C
  • measure_theory.integral.lebesgue_normed_space
  • measure_theory.integral.riesz_markov_kakutani
  • measure_theory.measure.content
  • measure_theory.measure.giry_monad
  • number_theory.legendre_symbol.zmod_char
  • number_theory.padics.padic_numbers
  • order.interval
  • ring_theory.algebraic
  • ring_theory.artinian
  • ring_theory.discrete_valuation_ring.basic
  • ring_theory.graded_algebra.radical
  • ring_theory.integral_closure
  • ring_theory.localization.as_subring
  • ring_theory.localization.away.basic
  • ring_theory.localization.cardinality
  • ring_theory.localization.localization_localization
  • ring_theory.power_series.basic
  • ring_theory.power_series.well_known
  • ring_theory.witt_vector.witt_polynomial
  • topology.metric_space.metrizable
  • topology.metric_space.thickened_indicator
  • topology.sheaves.punit
  • topology.urysohns_bounded
  • topology.vector_bundle.basic
  • topology.vector_bundle.constructions

Estimated changes