Support

📁 Source: Mathlib/Data/Set/Pointwise/Support.lean

Statistics

Metric	Count
Definitions	0
Theorems mulSupport_comp_inv_smul, mulSupport_comp_inv_smul₀, support_comp_inv_smul, support_comp_inv_smul₀	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_comp_inv_smul 📖	mathematical	—	Function.mulSupport SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set Set.smulSet	—	Set.ext
mulSupport_comp_inv_smul₀ 📖	mathematical	—	Function.mulSupport SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Set Set.smulSet	—	Set.ext Set.mem_smul_set_iff_inv_smul_mem₀
support_comp_inv_smul 📖	mathematical	—	Function.support SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set Set.smulSet	—	Set.ext
support_comp_inv_smul₀ 📖	mathematical	—	Function.support SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Set Set.smulSet	—	Set.ext Set.mem_smul_set_iff_inv_smul_mem₀

---

← Back to Index