Pretransitive

📁 Source: Mathlib/Algebra/Group/Action/Pretransitive.lean

Statistics

Metric	Count
Definitions IsPretransitive, IsPretransitive	2
Theorems exists_vadd_eq, of_vaddAssocClass, of_vadd_eq, isPretransitive, isPretransitive_addOpposite, exists_vadd_eq, instIsPretransitiveOfSubsingleton, isPretransitive_iff, surjective_vadd, addAction_isPretransitive, exists_smul_eq, of_isScalarTower, of_smul_eq, isPretransitive, isPretransitive_mulOpposite, exists_smul_eq, instIsPretransitiveOfSubsingleton, isPretransitive_iff, surjective_smul, mulAction_isPretransitive	20
Total	22

AddAction

Definitions

Name	Category	Theorems
IsPretransitive 📖	CompData	31 math math: IsPretransitive.of_embedding, IsPretransitive.of_vaddAssocClass, SeparationQuotient.instIsPretransitiveVAdd, IsPretransitive.of_surjective_map, pretransitive_iff_unique_quotient_of_nonempty, isPretransitive_compHom, IsQuasiPreprimitive.isPretransitive_of_normal, SubAddAction.ofStabilizer.isPretransitive_iff, pretransitive_iff_subsingleton_quotient, Regular.isPretransitive, Set.powersetCard.isPretransitive_of_isMultiplyPretransitive', isPretransitive_of_is_two_pretransitive, zeroEmbedding_isPretransitive_iff, isPretransitive_iff_orbit_eq_univ, is_zero_pretransitive, IsPreprimitive.toIsPretransitive, IsPretransitive.of_embedding_congr, IsPretransitive.of_compHom, instIsPretransitiveOfSubsingleton, IsPretransitive.of_vadd_eq, instIsPretransitiveElemOrbit, isPretransitive_iff, isPretransitive_congr, Regular.isPretransitive_addOpposite, Additive.addAction_isPretransitive, instIsPretransitiveElemOrbit_1, is_zero_pretransitive_iff, IsQuasiPreprimitive.toIsPretransitive, isPretransitive_quotient, isPretransitive_iff_base, SubAddAction.ofStabilizer.isPretransitive_iff_of_conj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_vadd_eq 📖	mathematical	—	HVAdd.hVAdd instHVAdd	—	IsPretransitive.exists_vadd_eq
instIsPretransitiveOfSubsingleton 📖	mathematical	—	IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	zero_vadd
isPretransitive_iff 📖	mathematical	—	IsPretransitive HVAdd.hVAdd instHVAdd	—	—
surjective_vadd 📖	mathematical	—	HVAdd.hVAdd instHVAdd	—	exists_vadd_eq

AddAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_vadd_eq 📖	mathematical	—	HVAdd.hVAdd instHVAdd	—	—
of_vaddAssocClass 📖	mathematical	—	AddAction.IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	of_vadd_eq vadd_zero_vadd
of_vadd_eq 📖	mathematical	HVAdd.hVAdd instHVAdd	AddAction.IsPretransitive	—	exists_vadd_eq

AddAction.Regular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPretransitive 📖	mathematical	—	AddAction.IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	neg_add_cancel_right
isPretransitive_addOpposite 📖	mathematical	—	AddAction.IsPretransitive AddOpposite Add.toVAddAddOpposite AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	add_neg_cancel_left

Additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addAction_isPretransitive 📖	mathematical	—	AddAction.IsPretransitive Additive vadd SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	MulAction.exists_smul_eq

MulAction

Definitions

Name	Category	Theorems
IsPretransitive 📖	CompData	54 math math: SubMulAction.ofStabilizer.isPretransitive_iff_of_conj, isPretransitive_iff_orbit_eq_univ, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, Set.powersetCard.isPretransitive, IsQuasiPreprimitive.isPretransitive_of_normal, SubMulAction.ofStabilizer.isPretransitive_iff, instIsPretransitiveElemOrbit_1, Set.powersetCard.isPretransitive_alternatingGroup, Multiplicative.mulAction_isPretransitive, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.transitive_of_isGalois, isPretransitive_iff_base, oneEmbedding_isPretransitive_iff, Regular.isPretransitive_mulOpposite, is_zero_pretransitive, isPretransitive_compHom, isPretransitive_quotient, instIsPretransitiveOfSubsingleton, Ideal.isPretransitive_of_isGalois, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected, IsQuasiPreprimitive.toIsPretransitive, Ideal.isPretransitive_of_isGaloisGroup, IsPretransitive.of_isScalarTower, Subgroup.isPretransitive_of_stabilizer_lt, instIsPretransitiveElemOrbit, SeparationQuotient.instIsPretransitiveSMul, CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective, IsPretransitive.of_embedding, isPretransitive_congr, IsPretransitive.of_compHom, Equiv.Perm.isPretransitive_of_isCycle_mem, CategoryTheory.PreGaloisCategory.instIsPretransitiveCarrierObjFintypeCatOfIsConnected, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, IsPretransitive.of_smul_eq, Polynomial.Gal.galAction_isPretransitive, AlternatingGroup.isPretransitive_of_three_le_card, isPretransitive_of_is_two_pretransitive, CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive, Set.powersetCard.isPretransitive_of_isMultiplyPretransitive, IsPretransitive.of_surjective_map, pretransitive_iff_subsingleton_quotient, Sylow.isPretransitive_of_finite, alternatingGroup.isPretransitive_of_three_le_card, Equiv.Perm.instIsPretransitive, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois, IsPreprimitive.toIsPretransitive, CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois, is_one_pretransitive_iff, isPretransitive_iff, pretransitive_iff_unique_quotient_of_nonempty, Regular.isPretransitive, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, IsPretransitive.of_embedding_congr, IsPretransitive.of_partition, SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_eq 📖	—	—	—	—	IsPretransitive.exists_smul_eq
instIsPretransitiveOfSubsingleton 📖	mathematical	—	IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	one_smul
isPretransitive_iff 📖	mathematical	—	IsPretransitive	—	—
surjective_smul 📖	—	—	—	—	exists_smul_eq

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_smul_eq 📖	—	—	—	—	—
of_isScalarTower 📖	mathematical	—	MulAction.IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	of_smul_eq smul_one_smul
of_smul_eq 📖	mathematical	—	MulAction.IsPretransitive	—	exists_smul_eq

MulAction.Regular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPretransitive 📖	mathematical	—	MulAction.IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction Monoid.toMulAction	—	inv_mul_cancel_right
isPretransitive_mulOpposite 📖	mathematical	—	MulAction.IsPretransitive MulOpposite Mul.toSMulMulOpposite MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul_inv_cancel_left

Multiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulAction_isPretransitive 📖	mathematical	—	MulAction.IsPretransitive Multiplicative smul AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	AddAction.exists_vadd_eq

---

← Back to Index