Documentation Verification Report

Hom

📁 Source: Mathlib/Algebra/Group/Nat/Hom.lean

Statistics

Metric	Count
Definitions `multiplesAddHom`, `multiplesHom`, `powersHom`, `powersMulHom`	4
Theorems `apply_nat`, `ext_nat`, `ext_nat_iff`, `apply_mnat`, `ext_mnat`, `ext_mnat_iff`, `ext_nat'`, `multiplesAddHom_apply`, `multiplesAddHom_symm_apply`, `multiplesHom_apply`, `multiplesHom_symm_apply`, `powersHom_apply`, `powersHom_symm_apply`, `powersMulHom_apply`, `powersMulHom_symm_apply`	15
Total	19

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_nat` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `instFunLike` `AddMonoid.toNatSMul`	—	`multiplesHom_symm_apply` `multiplesHom_apply` `Equiv.apply_symm_apply`
`ext_nat` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `instFunLike`	—	—	`ext_nat'` `instAddMonoidHomClass`
`ext_nat_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `instFunLike`	—	`ext_nat`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mnat` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `instFunLike` `Monoid.toNatPow` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd` `Multiplicative.toAdd`	—	`powersHom_symm_apply` `powersHom_apply` `Equiv.apply_symm_apply`
`ext_mnat` 📖	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—	`ext` `apply_mnat`
`ext_mnat_iff` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	`ext_mnat`

(root)

Definitions

Name	Category	Theorems
`multiplesAddHom` 📖	CompOp	2 math math: `multiplesAddHom_apply`, `multiplesAddHom_symm_apply`
`multiplesHom` 📖	CompOp	3 math math: `AddSubmonoid.closure_singleton_eq`, `multiplesHom_symm_apply`, `multiplesHom_apply`
`powersHom` 📖	CompOp	4 math math: `Polynomial.eval₂_ofFinsupp`, `powersHom_symm_apply`, `Submonoid.closure_singleton_eq`, `powersHom_apply`
`powersMulHom` 📖	CompOp	2 math math: `powersMulHom_apply`, `powersMulHom_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_nat'` 📖	—	`DFunLike.coe`	—	—	`DFunLike.ext` `map_zero` `AddMonoidHomClass.toZeroHomClass` `map_add` `AddMonoidHomClass.toAddHomClass`
`multiplesAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `multiplesAddHom` `AddMonoid.toNatSMul`	—	—
`multiplesAddHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidHom.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `multiplesAddHom` `AddMonoidHom.instFunLike`	—	—
`multiplesHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `multiplesHom` `AddMonoid.toNatSMul`	—	—
`multiplesHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `multiplesHom` `AddMonoidHom.instFunLike`	—	—
`powersHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `powersHom` `Monoid.toNatPow` `Multiplicative.toAdd`	—	—
`powersHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `powersHom` `MonoidHom.instFunLike` `Multiplicative.ofAdd`	—	—
`powersMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.instFunLike` `MulEquiv` `MulOne.toMul` `MonoidHom.mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `powersMulHom` `Monoid.toNatPow` `Equiv` `Equiv.instEquivLike` `Multiplicative.toAdd`	—	—
`powersMulHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MonoidHom.mul` `MulOne.toMul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `powersMulHom` `MonoidHom.instFunLike` `Equiv` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—

---

← Back to Index