Commit 2023-03-27 10:38 2d6e2be1

View on Github →

sync: update sha from backports (#3079) These files have been primarily modified by backports and need little modification:

  • topology.basic: #1826 - modified with a porting note, which can now be removed
  • data.real.cau_seq_completion: #1469 - not a backport, but forgot to update the SHA
  • order.filter.n_ary.basic: #1967 - this PR forgot to update the SHA
  • ring_theory.valuation.basic: The change is a small golf that is now included in this PR

Estimated changes