Combination

📁 Source: Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

Statistics

Metric	Count
Definitions addActionHom_of_embedding, addActionHom_singleton, instAddActionElemFinset, instMulActionElemFinset, mulActionHom_compl, mulActionHom_of_embedding, mulActionHom_singleton, subAddAction, subMulAction	9
Theorems addActionHom_of_embedding_surjective, addActionHom_singleton_bijective, addAction_faithful, addAction_stabilizer_coe, coe_addActionHom_of_embedding, coe_mulActionHom_compl, coe_mulActionHom_of_embedding, coe_smul, coe_vadd, faithfulSMul, faithfulVAdd, isPreprimitive_alternatingGroup, isPreprimitive_perm, isPretransitive, isPretransitive_alternatingGroup, isPretransitive_of_isMultiplyPretransitive, isPretransitive_of_isMultiplyPretransitive', mem_mulActionHom_compl, mulActionHom_compl_bijective, mulActionHom_compl_mulActionHom_compl, mulActionHom_of_embedding_surjective, mulActionHom_singleton_bijective, mulAction_faithful, stabilizer_coe	24
Total	33

Set.powersetCard

Definitions

Name	Category	Theorems
addActionHom_of_embedding 📖	CompOp	2 math math: addActionHom_of_embedding_surjective, coe_addActionHom_of_embedding
addActionHom_singleton 📖	CompOp	1 math math: addActionHom_singleton_bijective
instAddActionElemFinset 📖	CompOp	8 math math: isPretransitive_of_isMultiplyPretransitive', addAction_stabilizer_coe, addActionHom_of_embedding_surjective, faithfulVAdd, addActionHom_singleton_bijective, coe_addActionHom_of_embedding, addAction_faithful, coe_vadd
instMulActionElemFinset 📖	CompOp	16 math math: isPretransitive, mem_mulActionHom_compl, faithfulSMul, stabilizer_coe, isPretransitive_alternatingGroup, mulActionHom_compl_mulActionHom_compl, mulActionHom_compl_bijective, isPreprimitive_perm, isPretransitive_of_isMultiplyPretransitive, isPreprimitive_alternatingGroup, mulActionHom_singleton_bijective, mulAction_faithful, coe_mulActionHom_compl, coe_mulActionHom_of_embedding, mulActionHom_of_embedding_surjective, coe_smul
mulActionHom_compl 📖	CompOp	4 math math: mem_mulActionHom_compl, mulActionHom_compl_mulActionHom_compl, mulActionHom_compl_bijective, coe_mulActionHom_compl
mulActionHom_of_embedding 📖	CompOp	2 math math: coe_mulActionHom_of_embedding, mulActionHom_of_embedding_surjective
mulActionHom_singleton 📖	CompOp	1 math math: mulActionHom_singleton_bijective
subAddAction 📖	CompOp	—
subMulAction 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addActionHom_of_embedding_surjective 📖	mathematical	—	Function.Embedding Set.Elem Finset Set.powersetCard DFunLike.coe AddActionHom Function.Embedding.vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset instFunLikeAddActionHom addActionHom_of_embedding	—	Function.Embedding.exists_of_card_eq_finset Fintype.card_fin
addActionHom_singleton_bijective 📖	mathematical	—	Function.Bijective Set.Elem Finset Set.powersetCard DFunLike.coe AddActionHom AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset instFunLikeAddActionHom addActionHom_singleton	—	Finset.singleton_injective Finset.card_eq_one
addAction_faithful 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast ENat.card	AddAction.toPerm Set.Elem Finset Set.powersetCard instAddActionElemFinset Equiv.Perm Equiv.Perm.instOne	—	Mathlib.Tactic.Contrapose.contrapose₁ exists_mem_notMem Equiv.ext_iff Mathlib.Tactic.Contrapose.contrapose₄ Equiv.Perm.coe_one coe_vadd
addAction_stabilizer_coe 📖	mathematical	—	AddAction.stabilizer Set.Elem Finset Set.powersetCard instAddActionElemFinset Set Set.addActionSet SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.coe instSetLikeElemFinset	—	AddSubgroup.ext AddAction.mem_stabilizer_iff coe_vadd Finset.coe_vadd_finset
coe_addActionHom_of_embedding 📖	mathematical	—	Finset Set Set.instMembership Set.powersetCard AddActionHom.toFun Function.Embedding Function.Embedding.vadd Set.Elem AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset addActionHom_of_embedding Finset.map Finset.univ Fin.fintype	—	—
coe_mulActionHom_compl 📖	mathematical	Fintype.card	Finset Set Set.instMembership Set.powersetCard DFunLike.coe MulActionHom Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset instFunLikeMulActionHom mulActionHom_compl Compl.compl BooleanAlgebra.toCompl Finset.booleanAlgebra	—	—
coe_mulActionHom_of_embedding 📖	mathematical	—	Finset Set Set.instMembership Set.powersetCard MulActionHom.toFun Function.Embedding Function.Embedding.smul Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset mulActionHom_of_embedding Finset.map Finset.univ Fin.fintype	—	—
coe_smul 📖	mathematical	—	Finset Set Set.instMembership Set.powersetCard Set.Elem SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset Finset.smulFinset	—	SubMulAction.val_smul
coe_vadd 📖	mathematical	—	Finset Set Set.instMembership Set.powersetCard HVAdd.hVAdd Set.Elem instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset Finset.vaddFinset	—	SubAddAction.val_vadd
faithfulSMul 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast ENat.card	FaithfulSMul Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset	—	faithfulSMul_iff MulAction.toPerm_injective MulAction.toPerm_one mulAction_faithful Equiv.Perm.ext_iff
faithfulVAdd 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast ENat.card	FaithfulVAdd Set.Elem Finset Set.powersetCard AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset	—	faithfulVAdd_iff AddAction.toPerm_injective AddAction.toPerm_zero addAction_faithful Equiv.Perm.ext_iff
isPreprimitive_alternatingGroup 📖	mathematical	Nat.card	MulAction.IsPreprimitive Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction instMulActionElemFinset Equiv.Perm.applyMulAction	—	isPretransitive_alternatingGroup le_trans LT.lt.le nontrivial lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat ENat.card_eq_coe_fintype_card IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Nat.card_eq_fintype_card Nontrivial.to_nonempty MulAction.isCoatom_stabilizer_iff_preprimitive stabilizer_coe alternatingGroup.isCoatom_stabilizer coe_nonempty_iff Mathlib.Meta.NormNum.isNat_le_true Finite.of_fintype ncard_eq ne_of_lt
isPreprimitive_perm 📖	mathematical	Nat.card	MulAction.IsPreprimitive Equiv.Perm Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MulAction.toSemigroupAction instMulActionElemFinset Equiv.Perm.applyMulAction	—	Nat.finite_of_card_ne_zero isPretransitive nontrivial' Nontrivial.to_nonempty MulAction.isCoatom_stabilizer_iff_preprimitive stabilizer_coe Equiv.Perm.isCoatom_stabilizer coe_nonempty_iff Set.nonempty_compl Set.eq_univ_iff_ncard ncard_eq LT.lt.ne
isPretransitive 📖	mathematical	—	MulAction.IsPretransitive Equiv.Perm Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup MulAction.toSemigroupAction instMulActionElemFinset Equiv.Perm.applyMulAction	—	isPretransitive_of_isMultiplyPretransitive Equiv.Perm.isMultiplyPretransitive
isPretransitive_alternatingGroup 📖	mathematical	Nat.card	MulAction.IsPretransitive Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction MulAction.instMulAction instMulActionElemFinset Equiv.Perm.applyMulAction	—	isPretransitive_of_isMultiplyPretransitive eq_or_ne MulAction.instIsPretransitiveOfSubsingleton Unique.instSubsingleton Fin.isEmpty' MulAction.is_one_pretransitive_iff alternatingGroup.isPretransitive_of_three_le_card alternatingGroup.isMultiplyPretransitive MulAction.isMultiplyPretransitive_of_le Finite.of_fintype MulAction.IsPretransitive.of_surjective_map Nat.card_eq_fintype_card add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Function.Bijective.surjective mulActionHom_compl_bijective Finite.card_le_one_iff_subsingleton instFiniteElemFinset card Nat.choose_eq_zero_iff not_le
isPretransitive_of_isMultiplyPretransitive 📖	mathematical	—	MulAction.IsPretransitive Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset	—	MulAction.IsPretransitive.of_surjective_map mulActionHom_of_embedding_surjective
isPretransitive_of_isMultiplyPretransitive' 📖	mathematical	—	AddAction.IsPretransitive Set.Elem Finset Set.powersetCard AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instAddActionElemFinset	—	AddAction.IsPretransitive.of_surjective_map addActionHom_of_embedding_surjective
mem_mulActionHom_compl 📖	mathematical	Fintype.card	Set.Elem Finset Set.powersetCard SetLike.instMembership instSetLikeElemFinset DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset instFunLikeMulActionHom mulActionHom_compl	—	Finset.mem_compl
mulActionHom_compl_bijective 📖	mathematical	Fintype.card	Function.Bijective Set.Elem Finset Set.powersetCard DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset instFunLikeMulActionHom mulActionHom_compl	—	Function.bijective_iff_has_inverse CompTriple.instId_comp CompTriple.instIsIdId DFunLike.ext_iff mulActionHom_compl_mulActionHom_compl
mulActionHom_compl_mulActionHom_compl 📖	mathematical	Fintype.card	MulActionHom.comp Set.Elem Finset Set.powersetCard SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset mulActionHom_compl CompTriple.instId_comp CompTriple.instIsIdId MulActionHom.id	—	MulActionHom.ext CompTriple.instId_comp CompTriple.instIsIdId Finset.ext
mulActionHom_of_embedding_surjective 📖	mathematical	—	Function.Embedding Set.Elem Finset Set.powersetCard DFunLike.coe MulActionHom Function.Embedding.smul SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset instFunLikeMulActionHom mulActionHom_of_embedding	—	Function.Embedding.exists_of_card_eq_finset Fintype.card_fin
mulActionHom_singleton_bijective 📖	mathematical	—	Function.Bijective Set.Elem Finset Set.powersetCard DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instMulActionElemFinset instFunLikeMulActionHom mulActionHom_singleton	—	Finset.singleton_injective Finset.card_eq_one
mulAction_faithful 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast ENat.card	MulAction.toPerm Set.Elem Finset Set.powersetCard instMulActionElemFinset Equiv.Perm Equiv.Perm.instOne	—	Mathlib.Tactic.Contrapose.contrapose₁ exists_mem_notMem Equiv.ext_iff Mathlib.Tactic.Contrapose.contrapose₄ Equiv.Perm.coe_one coe_smul
stabilizer_coe 📖	mathematical	—	MulAction.stabilizer Set.Elem Finset Set.powersetCard instMulActionElemFinset Set Set.mulActionSet DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.coe instSetLikeElemFinset	—	Subgroup.ext coe_smul Finset.coe_smul_finset

---

← Back to Index