Documentation Verification Report

Single

📁 Source: Mathlib/Algebra/SkewMonoidAlgebra/Single.lean

Statistics

Metric	Count
Definitions `erase`, `update`	2
Theorems `coeff_erase_apply`, `coeff_erase_ne`, `coeff_erase_same`, `coeff_update`, `coeff_update_apply`, `coeff_update_ne`, `coeff_update_same`, `erase_apply_toFinsupp`, `erase_single`, `induction`, `single_add_erase`, `support_erase`, `support_update`, `update_eq_erase_add_single`, `update_self`, `update_toFinsupp`, `update_zero_eq_erase`, `zero_update`	18
Total	20

SkewMonoidAlgebra

Definitions

Name	Category	Theorems
`erase` 📖	CompOp	9 math math: `erase_apply_toFinsupp`, `coeff_erase_same`, `coeff_erase_ne`, `update_eq_erase_add_single`, `update_zero_eq_erase`, `erase_single`, `single_add_erase`, `coeff_erase_apply`, `support_erase`
`update` 📖	CompOp	10 math math: `coeff_update_ne`, `update_self`, `update_eq_erase_add_single`, `zero_update`, `update_toFinsupp`, `update_zero_eq_erase`, `coeff_update_apply`, `coeff_update_same`, `support_update`, `coeff_update`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_erase_apply` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `erase`	—	—
`coeff_erase_ne` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `erase`	—	`Finsupp.erase_ne`
`coeff_erase_same` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `erase`	—	`Finsupp.erase_same`
`coeff_update` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `update` `Function.update`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`coeff_update_apply` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `update`	—	`coeff_update` `Function.update_apply`
`coeff_update_ne` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `update`	—	`coeff_update_apply`
`coeff_update_same` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `update`	—	`coeff_update_apply`
`erase_apply_toFinsupp` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `instAddMonoid` `AddMonoidHom.instFunLike` `erase` `Finsupp.erase`	—	—
`erase_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `erase` `single` `instZero`	—	`Finsupp.erase_single`
`induction` 📖	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZero` `instAdd` `single`	—	—	`Finset.cons_induction_on` `support_eq_empty` `support_erase` `Finset.mem_erase` `Finset.erase_cons` `single_add_erase`
`single_add_erase` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `single` `coeff` `DFunLike.coe` `AddMonoidHom` `instAddMonoid` `AddMonoidHom.instFunLike` `erase`	—	`toFinsupp_injective` `single.eq_1` `toFinsupp_apply` `toFinsupp_add` `erase_apply_toFinsupp` `Finsupp.single_add_erase`
`support_erase` 📖	mathematical	—	`support` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `erase` `Finset.erase`	—	`Finset.ext` `support_ofFinsupp` `Finsupp.support_erase`
`support_update` 📖	mathematical	—	`support` `AddCommMonoid.toAddMonoid` `update` `Finset` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finset.erase` `Finset.instInsert`	—	`support_ofFinsupp` `Finsupp.support_update_ne_zero` `Finsupp.support_update_zero`
`update_eq_erase_add_single` 📖	mathematical	—	`update` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAdd` `DFunLike.coe` `AddMonoidHom` `instAddMonoid` `AddMonoidHom.instFunLike` `erase` `single`	—	`ext` `coeff_update_same` `coeff_add` `coeff_erase_same` `coeff_single_apply` `zero_add` `coeff_update_ne` `coeff_erase_ne` `add_zero`
`update_self` 📖	mathematical	—	`update` `coeff` `AddCommMonoid.toAddMonoid`	—	`toFinsupp_injective` `Finsupp.update_self`
`update_toFinsupp` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `update` `Finsupp.update`	—	—
`update_zero_eq_erase` 📖	mathematical	—	`update` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `instAddMonoid` `AddMonoidHom.instFunLike` `erase`	—	`ext` `coeff_update_apply` `coeff_erase_apply`
`zero_update` 📖	mathematical	—	`update` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZero` `single`	—	—

---

← Back to Index