Commit 2024-03-27 11:32 48efc23f

View on Github →

chore(Data/Nat/Factorial): Use Std lemmas (#11715) Make use of Nat-specific lemmas from Std rather than the general ones provided by mathlib. The ultimate goal here is to carve out Data, Algebra and Order sublibraries.

Estimated changes