Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 11:52 c7c40a7d

View on Github →

feat(*/pi): add lemmas about how single interacts with operators (#6317) This also adds a missing pi instances for monoid_with_zero.

Estimated changes

modified def add_monoid_hom.single
added def mul_hom.single
added theorem pi.single_add
added theorem pi.single_mul
added theorem pi.single_neg
added theorem pi.single_sub
added theorem pi.single_zero
added theorem pi.single_smul'
added theorem pi.single_smul
added theorem pi.apply_single
added theorem pi.apply_single₂