Documentation Verification Report

Lift

📁 Source: Mathlib/Algebra/MonoidAlgebra/Lift.lean

Statistics

Metric	Count
Definitions `liftNC`, `liftNCRingHom`, `liftNC`, `liftNCRingHom`	4
Theorems `liftNCRingHom_single`, `liftNC_mul`, `liftNC_one`, `liftNC_single`, `liftNCRingHom_single`, `liftNC_mul`, `liftNC_one`, `liftNC_single`	8
Total	12

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`liftNC` 📖	CompOp	7 math math: `liftNC_mul`, `Polynomial.eval₂_ofFinsupp`, `coe_liftNCAlgHom`, `liftNC_smul`, `liftNC_single`, `liftNC_one`, `lift_def`
`liftNCRingHom` 📖	CompOp	1 math math: `liftNCRingHom_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftNCRingHom_single` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike`	`DFunLike.coe` `RingHom` `AddMonoidAlgebra` `nonAssocSemiring` `AddMonoid.toAddZeroClass` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `liftNCRingHom` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MonoidHom` `Multiplicative` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	`liftNC_single`
`liftNC_mul` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finsupp.instFunLike` `Multiplicative` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Multiplicative` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`MonoidAlgebra.liftNC_mul`
`liftNC_one` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Multiplicative` `zero` `AddMonoidWithOne.toOne`	—	`MonoidAlgebra.liftNC_one`
`liftNC_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddMonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `liftNC` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Equiv` `Multiplicative` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	`Finsupp.liftAddHom_apply_single`

MonoidAlgebra

Definitions

Name	Category	Theorems
`liftNC` 📖	CompOp	6 math math: `liftNC_mul`, `coe_liftNCAlgHom`, `liftNC_single`, `liftNC_smul`, `lift_def`, `liftNC_one`
`liftNCRingHom` 📖	CompOp	1 math math: `liftNCRingHom_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftNCRingHom_single` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike`	`DFunLike.coe` `RingHom` `MonoidAlgebra` `nonAssocSemiring` `Monoid.toMulOneClass` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `liftNCRingHom` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike`	—	`liftNC_single`
`liftNC_mul` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finsupp.instFunLike`	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sum_single` `mul_def` `map_finsuppSum` `AddMonoidHom.instAddMonoidHomClass` `liftNC_single` `Finsupp.sum_mul` `Finsupp.mul_sum` `Finset.sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `Commute.left_comm`
`liftNC_one` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `one` `AddMonoidWithOne.toOne`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `liftNC_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_one`
`liftNC_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MonoidAlgebra` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `liftNC` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`Finsupp.liftAddHom_apply_single`

---

← Back to Index