Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 21:29 44e2d1e4

View on Github →

chore(algebra/support): golf, use to_additive (#17711)

Estimated changes

Modified src/algebra/support.lean

added theorem pi.mul_support_mul_single

added theorem pi.mul_support_mul_single_disjoint

added theorem pi.mul_support_mul_single_of_ne

added theorem pi.mul_support_mul_single_one

added theorem pi.mul_support_mul_single_subset

deleted theorem pi.support_single

deleted theorem pi.support_single_disjoint

deleted theorem pi.support_single_of_ne

deleted theorem pi.support_single_subset

deleted theorem pi.support_single_zero