Support

📁 Source: Mathlib/Algebra/Group/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems mulSupport_div, mulSupport_fun_inv, mulSupport_inv, mulSupport_mul, mulSupport_mul_inv, mulSupport_pow, support_add, support_add_neg, support_fun_neg, support_neg, support_nsmul, support_sub	12
Total	12

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_div 📖	mathematical	—	Set Set.instHasSubset mulSupport InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivInvMonoid.toDiv DivisionMonoid.toDivInvMonoid Set.instUnion	—	mulSupport_binop_subset one_div_one
mulSupport_fun_inv 📖	mathematical	—	mulSupport InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid InvOneClass.toInv	—	Set.ext inv_ne_one
mulSupport_inv 📖	mathematical	—	mulSupport InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Pi.instInv InvOneClass.toInv	—	mulSupport_fun_inv
mulSupport_mul 📖	mathematical	—	Set Set.instHasSubset mulSupport MulOne.toOne MulOneClass.toMulOne MulOne.toMul Set.instUnion	—	mulSupport_binop_subset one_mul
mulSupport_mul_inv 📖	mathematical	—	Set Set.instHasSubset mulSupport InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid DivisionMonoid.toDivInvMonoid InvOneClass.toInv Set.instUnion	—	mulSupport_binop_subset inv_one mul_one
mulSupport_pow 📖	mathematical	—	Set Set.instHasSubset mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Monoid.toNatPow	—	pow_zero mulSupport_fun_one pow_succ' HasSubset.Subset.trans Set.instIsTransSubset mulSupport_mul Set.union_subset Set.Subset.rfl
support_add 📖	mathematical	—	Set Set.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddZero.toAdd Set.instUnion	—	support_binop_subset zero_add
support_add_neg 📖	mathematical	—	Set Set.instHasSubset support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid SubtractionMonoid.toSubNegMonoid NegZeroClass.toNeg Set.instUnion	—	support_binop_subset neg_zero add_zero
support_fun_neg 📖	mathematical	—	support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid NegZeroClass.toNeg	—	Set.ext neg_ne_zero
support_neg 📖	mathematical	—	support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid Pi.instNeg NegZeroClass.toNeg	—	support_fun_neg
support_nsmul 📖	mathematical	—	Set Set.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoid.toNatSMul	—	zero_nsmul support_fun_zero Set.empty_subset succ_nsmul' HasSubset.Subset.trans Set.instIsTransSubset support_add Set.union_subset Set.Subset.rfl
support_sub 📖	mathematical	—	Set Set.instHasSubset support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubNegMonoid.toSub SubtractionMonoid.toSubNegMonoid Set.instUnion	—	support_binop_subset zero_sub_zero

---

← Back to Index