ViaEmbedding

📁 Source: Mathlib/GroupTheory/Perm/ViaEmbedding.lean

Statistics

Metric	Count
Definitions viaEmbedding, viaEmbeddingHom	2
Theorems viaEmbeddingHom_apply, viaEmbeddingHom_injective, viaEmbedding_apply, viaEmbedding_apply_of_notMem	4
Total	6

Equiv.Perm

Definitions

Name	Category	Theorems
viaEmbedding 📖	CompOp	3 math math: viaEmbeddingHom_apply, viaEmbedding_apply, viaEmbedding_apply_of_notMem
viaEmbeddingHom 📖	CompOp	2 math math: viaEmbeddingHom_apply, viaEmbeddingHom_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
viaEmbeddingHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup MonoidHom.instFunLike viaEmbeddingHom viaEmbedding	—	—
viaEmbeddingHom_injective 📖	mathematical	—	Equiv.Perm DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup MonoidHom.instFunLike viaEmbeddingHom	—	extendDomainHom_injective Function.Embedding.inj'
viaEmbedding_apply 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike viaEmbedding Function.Embedding Function.instFunLikeEmbedding	—	extendDomain_apply_image Function.Embedding.inj'
viaEmbedding_apply_of_notMem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike viaEmbedding	—	extendDomain_apply_not_subtype Function.Embedding.inj'

---

← Back to Index