Commit 2023-04-13 16:44 902ce181

View on Github →

chore: forward port mathlib#18668, 18781, 18783, 18792, 18794 (#3410)

  • set_theory.cardinal.basic: forward-ports leanprover-community/mathlib#18781, which backports some ad-hoc changes in #3247 in a more principled way
  • ring_theory.int.basic: these changes were already forward-ported in #3278, but we forgot the SHA.
  • linear_algebra.dimension: forward-ports leanprover-community/mathlib#18792
  • linear_algebra.matrix.dot_product: forward-ports leanprover-community/mathlib#18783
  • linear_algebra.finrank: forward-ports leanprover-community/mathlib#18794 which is itself a backport of #3378, hence no changes to the file

Estimated changes