Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-23 15:54 bb2e7f9e

View on Github →

feat(algebra/star/pi): star operates elementwise on pi types (#7342)

Estimated changes

modified theorem star_smul
added theorem pi.star_apply