Commit 2024-05-27 12:42 06ba8d8a

View on Github →

chore: Split Algebra.Function.Support/Algebra.Function.Indicator (#13244) ... in a file about Group and another one about GroupWithZero. Credit Yury for https://github.com/leanprover-community/mathlib/pull/2340 and Zhouhang for https://github.com/leanprover-community/mathlib/pull/1949.

Estimated changes

deleted theorem Set.indicator_mul
deleted theorem Set.indicator_mul_left
deleted theorem Set.indicator_mul_right
deleted theorem Set.indicator_one_inj
deleted theorem Set.indicator_prod_one
deleted theorem Set.inter_indicator_mul
deleted theorem Set.inter_indicator_one
modified def Function.mulSupport
deleted theorem Function.mulSupport_zero
deleted def Function.support
deleted theorem Function.support_div'
deleted theorem Function.support_div
deleted theorem Function.support_inv'
deleted theorem Function.support_inv
deleted theorem Function.support_mul'
deleted theorem Function.support_mul
deleted theorem Function.support_one
deleted theorem Function.support_pow'
deleted theorem Function.support_pow
added theorem Function.support_div'
added theorem Function.support_div
added theorem Function.support_inv'
added theorem Function.support_inv
added theorem Function.support_mul'
added theorem Function.support_mul
added theorem Function.support_one
added theorem Function.support_pow'
added theorem Function.support_pow
added theorem Set.indicator_mul
added theorem Set.indicator_mul_left
added theorem Set.indicator_one_inj
added theorem Set.indicator_prod_one