Subgroup

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

Statistics

Metric	Count
Definitions pointwiseMulAction	1
Theorems coe_pointwise_smul, le_pointwise_smul_iff, le_pointwise_smul_iff₀, mem_inv_pointwise_smul_iff, mem_inv_pointwise_smul_iff₀, mem_pointwise_smul_iff_inv_smul_mem, mem_pointwise_smul_iff_inv_smul_mem₀, mem_smul_pointwise_iff_exists, pointwise_isCentralScalar, pointwise_smul_def, pointwise_smul_le_iff, pointwise_smul_le_iff₀, pointwise_smul_le_pointwise_smul_iff, pointwise_smul_le_pointwise_smul_iff₀, pointwise_smul_toAddSubmonoid, smul_mem_pointwise_smul, smul_mem_pointwise_smul_iff, smul_mem_pointwise_smul_iff₀, le_pointwise_smul_iff₀, mem_inv_pointwise_smul_iff₀, mem_pointwise_smul_iff_inv_smul_mem₀, pointwise_smul_le_iff₀, pointwise_smul_le_pointwise_smul_iff₀, smul_mem_pointwise_smul_iff₀	24
Total	25

AddSubgroup

Definitions

Name	Category	Theorems
pointwiseMulAction 📖	CompOp	25 math math: zero_smul, smul_mem_pointwise_smul_iff, mem_inv_pointwise_smul_iff, Submodule.pointwise_smul_toAddSubgroup, Subring.pointwise_smul_toAddSubgroup, pointwise_smul_le_iff₀, relIndex_pointwise_smul, pointwise_smul_toAddSubmonoid, mem_smul_pointwise_iff_exists, mem_pointwise_smul_iff_inv_smul_mem, smul_mem_pointwise_smul, pointwise_smul_le_pointwise_smul_iff₀, smul_mem_pointwise_smul_iff₀, coe_pointwise_smul, pointwise_smul_le_pointwise_smul_iff, Ideal.pointwise_smul_toAddSubgroup, pointwise_smul_le_iff, mem_inv_pointwise_smul_iff₀, le_pointwise_smul_iff, AddCommGroup.smul_top_eq_top_of_divisibleBy_int, le_pointwise_smul_iff₀, pointwise_smul_def, pointwise_isCentralScalar, index_smul, mem_pointwise_smul_iff_inv_smul_mem₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pointwise_smul 📖	mathematical	—	SetLike.coe AddSubgroup instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
le_pointwise_smul_iff 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.subset_smul_set_iff
le_pointwise_smul_iff₀ 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.subset_smul_set_iff₀
mem_inv_pointwise_smul_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.mem_inv_smul_set_iff
mem_inv_pointwise_smul_iff₀ 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.mem_inv_smul_set_iff₀
mem_pointwise_smul_iff_inv_smul_mem 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem
mem_pointwise_smul_iff_inv_smul_mem₀ 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem₀
mem_smul_pointwise_iff_exists 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.mem_smul_set
pointwise_isCentralScalar 📖	mathematical	—	IsCentralScalar AddSubgroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction MulOpposite MulOpposite.instMonoid	—	AddMonoidHom.ext IsCentralScalar.op_smul_eq_smul
pointwise_smul_def 📖	mathematical	—	AddSubgroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction map DFunLike.coe MonoidHom AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MulOneClass.toMulOne Monoid.toMulOneClass AddMonoid.End.instMonoid MonoidHom.instFunLike DistribMulAction.toAddMonoidEnd	—	—
pointwise_smul_le_iff 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.smul_set_subset_iff_subset_inv_smul_set
pointwise_smul_le_iff₀ 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.smul_set_subset_iff₀
pointwise_smul_le_pointwise_smul_iff 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction	—	Set.smul_set_subset_smul_set_iff
pointwise_smul_le_pointwise_smul_iff₀ 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction	—	Set.smul_set_subset_smul_set_iff₀
pointwise_smul_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid AddSubgroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.pointwiseMulAction	—	—
smul_mem_pointwise_smul 📖	mathematical	AddSubgroup SetLike.instMembership instSetLike	SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.smul_mem_smul_set
smul_mem_pointwise_smul_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.smul_mem_smul_set_iff
smul_mem_pointwise_smul_iff₀ 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Set.smul_mem_smul_set_iff₀

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_pointwise_smul_iff₀ 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.subset_smul_set_iff₀
mem_inv_pointwise_smul_iff₀ 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Set.mem_inv_smul_set_iff₀
mem_pointwise_smul_iff_inv_smul_mem₀ 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.mem_smul_set_iff_inv_smul_mem₀
pointwise_smul_le_iff₀ 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	Set.smul_set_subset_iff₀
pointwise_smul_le_pointwise_smul_iff₀ 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction	—	Set.smul_set_subset_smul_set_iff₀
smul_mem_pointwise_smul_iff₀ 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Set.smul_mem_smul_set_iff₀

---

← Back to Index