mathlib

2b46eea7 - Change also the final lemmas to mul_indicator form with to_additive attributes.