Commit 2023-11-04 06:42 dd572a65

View on Github →

chore: minimize imports for simps (#8140)

Estimated changes

Modified Mathlib/Tactic/NormNum/Result.lean

Modified Mathlib/Tactic/Simps/Basic.lean

modified def Simps.findProjectionIndices

modified def Simps.getCompositeOfProjections

Modified Mathlib/Tactic/Simps/NotationClass.lean