Indicator

📁 Source: Mathlib/Algebra/GroupWithZero/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems mulSupport_add_one, mulSupport_add_one', mulSupport_one_add, mulSupport_one_add', mulSupport_one_sub, mulSupport_one_sub', mulSupport_zero, support_div, support_div', support_inv, support_inv', support_mul, support_mul', support_mul_of_ne_zero_left, support_mul_of_ne_zero_right, support_mul_subset_left, support_mul_subset_right, support_one, support_pow, support_pow', indicator_const_mul, indicator_eq_one_iff_mem, indicator_eq_zero_iff_notMem, indicator_mul, indicator_mul_const, indicator_mul_left, indicator_mul_right, indicator_one_inj, indicator_prod_one, inter_indicator_mul, inter_indicator_one	31
Total	31

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_add_one 📖	mathematical	—	mulSupport AddSemigroup.toAdd AddMonoid.toAddSemigroup AddRightCancelMonoid.toAddMonoid support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Set.ext add_eq_right AddRightCancelSemigroup.toIsRightCancelAdd
mulSupport_add_one' 📖	mathematical	—	mulSupport Pi.instAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup AddRightCancelMonoid.toAddMonoid Pi.instOne support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	mulSupport_add_one
mulSupport_one_add 📖	mathematical	—	mulSupport AddSemigroup.toAdd AddMonoid.toAddSemigroup AddLeftCancelMonoid.toAddMonoid support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Set.ext add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd
mulSupport_one_add' 📖	mathematical	—	mulSupport Pi.instAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup AddLeftCancelMonoid.toAddMonoid Pi.instOne support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	mulSupport_one_add
mulSupport_one_sub 📖	mathematical	—	mulSupport SubNegMonoid.toSub AddGroup.toSubNegMonoid support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	mulSupport_one_sub'
mulSupport_one_sub' 📖	mathematical	—	mulSupport Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid Pi.instOne support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	sub_eq_add_neg mulSupport_one_add' support_neg
mulSupport_zero 📖	mathematical	—	mulSupport Pi.instZero Set.univ	—	mulSupport_const zero_ne_one
support_div 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Set Set.instInter	—	div_eq_mul_inv support_mul IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero instIsCancelMulZero support_inv
support_div' 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Pi.instDiv DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid Set Set.instInter	—	support_div
support_inv 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.ext inv_eq_zero
support_inv' 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	support_inv
support_mul 📖	mathematical	—	support MulZeroClass.toZero MulZeroClass.toMul Set Set.instInter	—	Set.ext
support_mul' 📖	mathematical	—	support MulZeroClass.toZero Pi.instMul MulZeroClass.toMul Set Set.instInter	—	support_mul
support_mul_of_ne_zero_left 📖	mathematical	—	support MulZeroClass.toZero MulZeroClass.toMul	—	support_mul support_eq_univ Set.univ_inter
support_mul_of_ne_zero_right 📖	mathematical	—	support MulZeroClass.toZero MulZeroClass.toMul	—	support_mul support_eq_univ Set.inter_univ
support_mul_subset_left 📖	mathematical	—	Set Set.instHasSubset support MulZeroClass.toZero MulZeroClass.toMul	—	MulZeroClass.zero_mul
support_mul_subset_right 📖	mathematical	—	Set Set.instHasSubset support MulZeroClass.toZero MulZeroClass.toMul	—	MulZeroClass.mul_zero
support_one 📖	mathematical	—	support Pi.instOne Set.univ	—	support_const one_ne_zero
support_pow 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	Set.ext Iff.not pow_eq_zero_iff isReduced_of_noZeroDivisors
support_pow' 📖	mathematical	—	support MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid	—	support_pow

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indicator_const_mul 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroClass.toMul	—	indicator_mul_right
indicator_eq_one_iff_mem 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Set instMembership	—	indicator_apply NeZero.one
indicator_eq_zero_iff_notMem 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Set instMembership	—	indicator_apply NeZero.one
indicator_mul 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroClass.toMul	—	MulZeroClass.mul_zero
indicator_mul_const 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroClass.toMul	—	indicator_mul_left
indicator_mul_left 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroClass.toMul	—	MulZeroClass.zero_mul
indicator_mul_right 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroClass.toMul	—	MulZeroClass.mul_zero
indicator_one_inj 📖	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	—	ext indicator_eq_one_iff_mem
indicator_prod_one 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass SProd.sprod Set instSProd Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MulZeroClass.toMul	—	mul_one MulZeroClass.mul_zero
inter_indicator_mul 📖	mathematical	—	indicator MulZeroClass.toZero Set instInter MulZeroClass.toMul	—	indicator_indicator MulZeroClass.mul_zero MulZeroClass.zero_mul
inter_indicator_one 📖	mathematical	—	indicator MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Set instInter Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Pi.instMul MulZeroClass.toMul	—	one_mul

---

← Back to Index