Commit 2026-03-26 22:21 87a6ef22
View on Github →chore: import lemma in Mathlib.Init (#36943)
This is a follow up to #36316 (which added Type* to Mathlib.Init), adding the lemma command to Mathlib.Init. This lets us remove a bunch of imports.