Commit 2025-07-04 06:01 19f4ef2c

View on Github →

chore: bump toolchain to v4.22.0-rc3 (#26715)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Ring/Defs.lean

added theorem nsmul_eq_mul

Modified Mathlib/Algebra/Ring/GrindInstances.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

deleted theorem nsmul_eq_mul

Modified Mathlib/Data/Nat/Hyperoperation.lean

Modified Mathlib/Logic/Function/Defs.lean

Modified MathlibTest/ImplicitUniverses.lean

Modified lake-manifest.json

Modified lakefile.lean

Modified lean-toolchain

Modified scripts/lint-style.lean