Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Group/WithOne/Basic.lean

Statistics

Metric	Count
Definitions `withZeroCongr`, `withOneCongr`, `coeMulHom`, `instInvolutiveInv`, `mapMulHom`, `coeAddHom`, `instInvolutiveNeg`, `mapAddHom`	8
Theorems `withZeroCongr_apply`, `withZeroCongr_refl`, `withZeroCongr_symm`, `withZeroCongr_trans`, `withOneCongr_apply`, `withOneCongr_refl`, `withOneCongr_symm`, `withOneCongr_trans`, `coeMulHom_apply`, `lift_coe`, `lift_one`, `lift_symm_apply`, `lift_unique`, `mapMulHom_coe`, `mapMulHom_comp`, `mapMulHom_id`, `mapMulHom_inj`, `mapMulHom_injective`, `mapMulHom_injective'`, `mapMulHom_mapMulHom`, `coeAddHom_apply`, `lift_coe`, `lift_symm_apply`, `lift_unique`, `lift_zero`, `mapAddHom_coe`, `mapAddHom_comp`, `mapAddHom_id`, `mapAddHom_inj`, `mapAddHom_injective`, `mapAddHom_injective'`, `mapAddHom_mapAddHom`	32
Total	40

AddEquiv

Definitions

Name	Category	Theorems
`withZeroCongr` 📖	CompOp	4 math math: `withZeroCongr_apply`, `withZeroCongr_symm`, `withZeroCongr_refl`, `withZeroCongr_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withZeroCongr_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `WithZero` `WithZero.instAdd` `EquivLike.toFunLike` `instEquivLike` `withZeroCongr` `AddMonoidHom` `AddZeroClass.toAddZero` `WithZero.instAddZeroClass` `AddMonoidHom.instFunLike` `WithZero.mapAddHom` `toAddHom`	—	—
`withZeroCongr_refl` 📖	mathematical	—	`withZeroCongr` `refl` `WithZero` `WithZero.instAdd`	—	`toAddMonoidHom_injective` `WithZero.mapAddHom_id`
`withZeroCongr_symm` 📖	mathematical	—	`symm` `WithZero` `WithZero.instAdd` `withZeroCongr`	—	—
`withZeroCongr_trans` 📖	mathematical	—	`trans` `WithZero` `WithZero.instAdd` `withZeroCongr`	—	`toAddMonoidHom_injective` `WithZero.mapAddHom_comp`

MulEquiv

Definitions

Name	Category	Theorems
`withOneCongr` 📖	CompOp	4 math math: `withOneCongr_symm`, `withOneCongr_apply`, `withOneCongr_trans`, `withOneCongr_refl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withOneCongr_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `WithOne` `WithOne.instMul` `EquivLike.toFunLike` `instEquivLike` `withOneCongr` `MonoidHom` `MulOneClass.toMulOne` `WithOne.instMulOneClass` `MonoidHom.instFunLike` `WithOne.mapMulHom` `toMulHom`	—	—
`withOneCongr_refl` 📖	mathematical	—	`withOneCongr` `refl` `WithOne` `WithOne.instMul`	—	`toMonoidHom_injective` `WithOne.mapMulHom_id`
`withOneCongr_symm` 📖	mathematical	—	`symm` `WithOne` `WithOne.instMul` `withOneCongr`	—	—
`withOneCongr_trans` 📖	mathematical	—	`trans` `WithOne` `WithOne.instMul` `withOneCongr`	—	`toMonoidHom_injective` `WithOne.mapMulHom_comp`

WithOne

Definitions

Name	Category	Theorems
`coeMulHom` 📖	CompOp	2 math math: `coeMulHom_apply`, `lift_unique`
`instInvolutiveInv` 📖	CompOp	—
`mapMulHom` 📖	CompOp	9 math math: `mapMulHom_coe`, `mapMulHom_injective`, `mapMulHom_comp`, `mapMulHom_mapMulHom`, `mapMulHom_id`, `MulEquiv.withOneCongr_apply`, `MonCat.adjoinOne_map`, `mapMulHom_injective'`, `mapMulHom_inj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `WithOne` `instMul` `MulHom.funLike` `coeMulHom` `coe`	—	—
`lift_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `WithOne` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `Equiv` `MulHom` `MulOne.toMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `coe` `MulHom.funLike`	—	—
`lift_one` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `WithOne` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `Equiv` `MulHom` `MulOne.toMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `instOne` `MulOne.toOne`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `MulOne.toMul` `MulOneClass.toMulOne` `MulHom.funLike` `Equiv` `MonoidHom` `WithOne` `instMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `MonoidHom.instFunLike` `coe`	—	—
`lift_unique` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MulHom` `MulOne.toMul` `MulOneClass.toMulOne` `MonoidHom` `WithOne` `instMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `MulHom.comp` `MonoidHom.toMulHom` `coeMulHom`	—	`Equiv.apply_symm_apply`
`mapMulHom_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `WithOne` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `mapMulHom` `coe` `MulHom` `MulHom.funLike`	—	—
`mapMulHom_comp` 📖	mathematical	—	`mapMulHom` `MulHom.comp` `MonoidHom.comp` `WithOne` `MulOneClass.toMulOne` `instMulOneClass`	—	`MonoidHom.ext` `mapMulHom_mapMulHom`
`mapMulHom_id` 📖	mathematical	—	`mapMulHom` `MulHom.id` `MonoidHom.id` `WithOne` `MulOneClass.toMulOne` `instMulOneClass`	—	`MonoidHom.ext`
`mapMulHom_inj` 📖	mathematical	—	`mapMulHom`	—	`mapMulHom_injective'`
`mapMulHom_injective` 📖	mathematical	`DFunLike.coe` `MulHom` `MulHom.funLike`	`WithOne` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `mapMulHom`	—	—
`mapMulHom_injective'` 📖	mathematical	—	`MulHom` `MonoidHom` `WithOne` `MulOneClass.toMulOne` `instMulOneClass` `mapMulHom`	—	`MulHom.ext` `coe_injective`
`mapMulHom_mapMulHom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `WithOne` `MulOneClass.toMulOne` `instMulOneClass` `MonoidHom.instFunLike` `mapMulHom` `MulHom.comp`	—	—

WithZero

Definitions

Name	Category	Theorems
`coeAddHom` 📖	CompOp	2 math math: `lift_unique`, `coeAddHom_apply`
`instInvolutiveNeg` 📖	CompOp	—
`mapAddHom` 📖	CompOp	9 math math: `mapAddHom_comp`, `mapAddHom_id`, `AddEquiv.withZeroCongr_apply`, `mapAddHom_injective'`, `mapAddHom_coe`, `mapAddHom_inj`, `mapAddHom_injective`, `mapAddHom_mapAddHom`, `AddMonCat.adjoinZero_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `WithZero` `instAdd` `AddHom.funLike` `coeAddHom` `coe`	—	—
`lift_coe` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `Equiv` `AddHom` `AddZero.toAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `coe` `AddHom.funLike`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddHom.funLike` `Equiv` `AddMonoidHom` `WithZero` `instAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `AddMonoidHom.instFunLike` `coe`	—	—
`lift_unique` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidHom` `WithZero` `instAddZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `AddHom.comp` `AddMonoidHom.toAddHom` `coeAddHom`	—	`Equiv.apply_symm_apply`
`lift_zero` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `Equiv` `AddHom` `AddZero.toAdd` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `instZero` `AddZero.toZero`	—	—
`mapAddHom_coe` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `mapAddHom` `coe` `AddHom` `AddHom.funLike`	—	—
`mapAddHom_comp` 📖	mathematical	—	`mapAddHom` `AddHom.comp` `AddMonoidHom.comp` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass`	—	`AddMonoidHom.ext` `mapAddHom_mapAddHom`
`mapAddHom_id` 📖	mathematical	—	`mapAddHom` `AddHom.id` `AddMonoidHom.id` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass`	—	`AddMonoidHom.ext`
`mapAddHom_inj` 📖	mathematical	—	`mapAddHom`	—	`mapAddHom_injective'`
`mapAddHom_injective` 📖	mathematical	`DFunLike.coe` `AddHom` `AddHom.funLike`	`WithZero` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `mapAddHom`	—	—
`mapAddHom_injective'` 📖	mathematical	—	`AddHom` `AddMonoidHom` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass` `mapAddHom`	—	`AddHom.ext` `coe_injective`
`mapAddHom_mapAddHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WithZero` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoidHom.instFunLike` `mapAddHom` `AddHom.comp`	—	—

---

← Back to Index