Documentation Verification Report

Transitive

📁 Source: Mathlib/GroupTheory/GroupAction/Transitive.lean

Statistics

Metric	Count
Definitions `Transitive`	1
Theorems `of_surjective_map`, `isPretransitive_congr`, `isPretransitive_iff_base`, `isPretransitive_iff_orbit_eq_univ`, `of_surjective_map`, `isPretransitive_congr`, `isPretransitive_iff_base`, `isPretransitive_iff_orbit_eq_univ`	8
Total	9

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `instFunLikeAddActionHom`	`IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction`	—	`IsPretransitive.of_surjective_map` `Function.Bijective.surjective` `IsPretransitive.exists_vadd_eq` `Function.Bijective.injective` `AddActionSemiHomClass.map_vaddₛₗ` `instAddActionSemiHomClassAddActionHom`
`isPretransitive_iff_base` 📖	mathematical	—	`IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `HVAdd.hVAdd` `instHVAdd`	—	`exists_vadd_eq` `vadd_vadd` `neg_add_cancel_right`
`isPretransitive_iff_orbit_eq_univ` 📖	mathematical	—	`IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `orbit` `Set.univ`	—	`isPretransitive_iff_base` `Set.ext_iff` `Set.mem_univ` `mem_orbit_iff`

AddAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_surjective_map` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`AddAction.IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`exists_vadd_eq` `AddActionSemiHomClass.map_vaddₛₗ` `instAddActionSemiHomClassAddActionHom`

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `instFunLikeMulActionHom`	`IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction`	—	`IsPretransitive.of_surjective_map` `Function.Bijective.surjective` `IsPretransitive.exists_smul_eq` `Function.Bijective.injective` `MulActionSemiHomClass.map_smulₛₗ` `instMulActionSemiHomClassMulActionHom`
`isPretransitive_iff_base` 📖	mathematical	—	`IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`exists_smul_eq` `smul_smul` `inv_mul_cancel_right`
`isPretransitive_iff_orbit_eq_univ` 📖	mathematical	—	`IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `orbit` `Set.univ`	—	`isPretransitive_iff_base` `Set.ext_iff`

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_surjective_map` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`MulAction.IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`exists_smul_eq` `MulActionSemiHomClass.map_smulₛₗ` `instMulActionSemiHomClassMulActionHom`

(root)

Definitions

Name	Category	Theorems
`Transitive` 📖	MathDef	1 math math: `transitive_of_trans`

---

← Back to Index