Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 01:48 4daaff06

View on Github →

feat(data/nat/prime): factors sublist of product (#11104) This PR changes the existing factors_subset_right to give a stronger sublist conclusion (which trivially can be used to reproduce the subst version).

Estimated changes