Documentation Verification Report

Embedding

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

Statistics

Metric	Count
Definitions `instAddAction`, `instMulAction`, `smul`, `vadd`	4
Theorems `coe_smul`, `coe_vadd`, `instIsCentralScalar`, `instIsScalarTower`, `instSMulCommClass`, `instVAddCommClass`, `smul_apply`, `smul_def`, `vadd_apply`, `vadd_def`	10
Total	14

Function.Embedding

Definitions

Name	Category	Theorems
`instAddAction` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`smul` 📖	CompOp	18 math math: `coe_smul`, `smul_apply`, `instIsCentralScalar`, `Function.Injective.mulActionHom_embedding_apply`, `Function.Injective.mulActionHom_embedding_isInjective`, `SubMulAction.exists_smul_of_last_eq`, `MulAction.oneEmbedding_isPretransitive_iff`, `Function.Bijective.mulActionHom_embedding_isBijective`, `instSMulCommClass`, `MulAction.is_zero_pretransitive`, `smul_def`, `MulAction.IsPretransitive.of_embedding`, `MulAction.isMultiplyPretransitive_iff`, `MulActionHom.oneEmbeddingMap_bijective`, `instIsScalarTower`, `Set.powersetCard.coe_mulActionHom_of_embedding`, `Set.powersetCard.mulActionHom_of_embedding_surjective`, `MulAction.IsPretransitive.of_embedding_congr`
`vadd` 📖	CompOp	16 math math: `AddAction.IsPretransitive.of_embedding`, `vadd_apply`, `Set.powersetCard.addActionHom_of_embedding_surjective`, `AddAction.zeroEmbedding_isPretransitive_iff`, `AddAction.is_zero_pretransitive`, `instVAddCommClass`, `Function.Bijective.addActionHom_embedding_isBijective`, `Set.powersetCard.coe_addActionHom_of_embedding`, `AddAction.IsPretransitive.of_embedding_congr`, `Function.Injective.addActionHom_embedding_isInjective`, `coe_vadd`, `Function.Injective.addActionHom_embedding_apply`, `AddAction.isMultiplyPretransitive_iff`, `SubAddAction.exists_vadd_of_last_eq`, `vadd_def`, `AddActionHom.zeroEmbeddingMap_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `smul` `Function.hasSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`coe_vadd` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `HVAdd.hVAdd` `instHVAdd` `vadd` `Function.hasVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Function.Embedding` `smul` `MulOpposite` `MulOpposite.instGroup`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Function.Embedding` `smul`	—	`ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `Function.Embedding` `smul`	—	`ext` `SMulCommClass.smul_comm`
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `Function.Embedding` `vadd`	—	`ext` `VAddCommClass.vadd_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—
`smul_def` 📖	mathematical	—	`Function.Embedding` `smul` `trans` `Equiv.toEmbedding` `MulAction.toPerm`	—	—
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `HVAdd.hVAdd` `instHVAdd` `vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `Function.Embedding` `instHVAdd` `vadd` `trans` `Equiv.toEmbedding` `AddAction.toPerm`	—	—

---

← Back to Index