Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-07-14 14:19
1b34c450
View on Github →
feat(Algebra.IndicatorFunction): indicator of smul in a SMulWithZero context (
#5874
)
Estimated changes
Modified
Mathlib/Algebra/IndicatorFunction.lean
added
theorem
Set.indicator_smul_apply_left
added
theorem
Set.indicator_smul_const
added
theorem
Set.indicator_smul_const_apply
added
theorem
Set.indicator_smul_left
Modified
Mathlib/Algebra/Support.lean
added
theorem
Function.mulSupport_comp_eq_of_range_subset