Documentation Verification Report

Embedding

📁 Source: Mathlib/Algebra/Group/Embedding.lean

Statistics

Metric	Count
Definitions `addLeftEmbedding`, `addRightEmbedding`, `mulLeftEmbedding`, `mulRightEmbedding`	4
Theorems `addLeftEmbedding_apply`, `addLeftEmbedding_eq_addRightEmbedding`, `addRightEmbedding_apply`, `mulLeftEmbedding_apply`, `mulLeftEmbedding_eq_mulRightEmbedding`, `mulRightEmbedding_apply`	6
Total	10

(root)

Definitions

Name	Category	Theorems
`addLeftEmbedding` 📖	CompOp	18 math math: `Finset.range_add`, `Int.Ioo_eq_finset_map`, `addLeftEmbedding_apply`, `addLeftEmbedding_eq_addRightEmbedding`, `Finset.map_add_left_Ico`, `Int.Icc_eq_finset_map`, `Int.Ioc_eq_finset_map`, `Finset.map_add_left_Ioo`, `Finset.disjoint_range_addLeftEmbedding`, `Int.uIcc_eq_finset_map`, `addRothNumber_map_add_left`, `Finset.map_add_left_Ioc`, `Finset.map_add_left_Icc`, `Finset.range_add_eq_union`, `Int.Ico_eq_finset_map`, `AddMonoidAlgebra.support_single_mul`, `List.toFinsupp_append`, `MvPolynomial.support_X_mul`
`addRightEmbedding` 📖	CompOp	12 math math: `addRightEmbedding_apply`, `addLeftEmbedding_eq_addRightEmbedding`, `MvPolynomial.support_mul_X`, `Finset.piAntidiag_cons`, `Finset.map_add_right_Ico`, `Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding`, `Finset.map_add_right_Ioo`, `Finset.map_add_right_Ioc`, `Finset.map_add_right_Icc`, `addRothNumber_map_add_right`, `Finset.disjoint_range_addRightEmbedding`, `AddMonoidAlgebra.support_mul_single`
`mulLeftEmbedding` 📖	CompOp	5 math math: `SkewMonoidAlgebra.support_single_mul`, `mulRothNumber_map_mul_left`, `mulLeftEmbedding_eq_mulRightEmbedding`, `MonoidAlgebra.support_single_mul`, `mulLeftEmbedding_apply`
`mulRightEmbedding` 📖	CompOp	5 math math: `SkewMonoidAlgebra.support_mul_single`, `mulRightEmbedding_apply`, `mulLeftEmbedding_eq_mulRightEmbedding`, `MonoidAlgebra.support_mul_single`, `mulRothNumber_map_mul_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `addLeftEmbedding`	—	—
`addLeftEmbedding_eq_addRightEmbedding` 📖	mathematical	—	`addLeftEmbedding` `AddCommMagma.toAdd` `IsCancelAdd.toIsLeftCancelAdd` `addRightEmbedding` `IsCancelAdd.toIsRightCancelAdd`	—	`Function.Embedding.ext` `IsCancelAdd.toIsLeftCancelAdd` `IsCancelAdd.toIsRightCancelAdd` `add_comm`
`addRightEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `addRightEmbedding`	—	—
`mulLeftEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `mulLeftEmbedding`	—	—
`mulLeftEmbedding_eq_mulRightEmbedding` 📖	mathematical	—	`mulLeftEmbedding` `CommMagma.toMul` `IsCancelMul.toIsLeftCancelMul` `mulRightEmbedding` `IsCancelMul.toIsRightCancelMul`	—	`Function.Embedding.ext` `IsCancelMul.toIsLeftCancelMul` `IsCancelMul.toIsRightCancelMul` `mul_comm`
`mulRightEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `mulRightEmbedding`	—	—

---

← Back to Index