Commit 2024-10-28 09:08 73203f9a
View on Github →chore: import Mathlib.Init in all files (#18277) This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
chore: import Mathlib.Init in all files (#18277) This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.