Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/SkewPolynomial/Basic.lean

Statistics

Metric	Count
Definitions `SkewPolynomial`, `instAddCommMonoid`, `instInhabited`, `instModule`, `instSMulZeroClass`, `instSemiring`, `instUniqueOfSubsingleton`, `monomial`, `support`, `φ`	10
Theorems `card_support_eq_zero`, `instIsScalarTower`, `instSMulCommClass`, `monomial_add`, `monomial_def`, `monomial_mul_monomial`, `monomial_zero_one`, `monomial_zero_right`, `smul_monomial`, `support_add`, `support_eq_empty`, `support_zero`, `φ_def`, `φ_iterate_apply`	14
Total	24

SkewPolynomial

Definitions

Name	Category	Theorems
`instAddCommMonoid` 📖	CompOp	12 math math: `monomial_add`, `monomial_def`, `card_support_eq_zero`, `support_zero`, `monomial_zero_one`, `monomial_zero_right`, `support_add`, `support_eq_empty`, `monomial_mul_monomial`, `instSMulCommClass`, `instIsScalarTower`, `smul_monomial`
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	7 math math: `monomial_add`, `monomial_def`, `monomial_zero_one`, `monomial_zero_right`, `monomial_mul_monomial`, `instSMulCommClass`, `smul_monomial`
`instSMulZeroClass` 📖	CompOp	2 math math: `instIsScalarTower`, `smul_monomial`
`instSemiring` 📖	CompOp	2 math math: `monomial_zero_one`, `monomial_mul_monomial`
`instUniqueOfSubsingleton` 📖	CompOp	—
`monomial` 📖	CompOp	6 math math: `monomial_add`, `monomial_def`, `monomial_zero_one`, `monomial_zero_right`, `monomial_mul_monomial`, `smul_monomial`
`support` 📖	CompOp	4 math math: `card_support_eq_zero`, `support_zero`, `support_add`, `support_eq_empty`
`φ` 📖	CompOp	3 math math: `φ_iterate_apply`, `φ_def`, `monomial_mul_monomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_support_eq_zero` 📖	mathematical	—	`Finset.card` `support` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid`	—	—
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instSMulZeroClass`	—	`SkewMonoidAlgebra.instIsScalarTower`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instModule`	—	`SkewMonoidAlgebra.instSMulCommClass`
`monomial_add` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`SkewMonoidAlgebra.single_add`
`monomial_def` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `SkewMonoidAlgebra.single` `Multiplicative` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—
`monomial_mul_monomial` 📖	mathematical	—	`SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `Nat.iterate` `RingHom` `RingHom.instFunLike` `φ`	—	`φ_iterate_apply` `SkewMonoidAlgebra.single_mul_single`
`monomial_zero_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instSemiring`	—	—
`monomial_zero_right` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`SkewMonoidAlgebra.single_zero`
`smul_monomial` 📖	mathematical	—	`SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toModule` `instModule` `LinearMap.instFunLike` `monomial`	—	`SkewMonoidAlgebra.smul_single`
`support_add` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `Finset.instUnion`	—	`SkewMonoidAlgebra.support_add`
`support_eq_empty` 📖	mathematical	—	`support` `Finset` `Finset.instEmptyCollection` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid`	—	—
`support_zero` 📖	mathematical	—	`support` `SkewPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Finset` `Finset.instEmptyCollection`	—	—
`φ_def` 📖	mathematical	—	`φ` `MulSemiringAction.toRingHom` `Multiplicative` `Multiplicative.monoid` `Nat.instAddMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	—
`φ_iterate_apply` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `φ` `Multiplicative` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Multiplicative.monoid` `Nat.instAddMonoid` `MulSemiringAction.toDistribMulAction` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Multiplicative.ofAdd`	—	`one_smul` `Function.iterate_succ'` `mul_comm`

(root)

Definitions

Name	Category	Theorems
`SkewPolynomial` 📖	CompOp	12 math math: `SkewPolynomial.monomial_add`, `SkewPolynomial.monomial_def`, `SkewPolynomial.card_support_eq_zero`, `SkewPolynomial.support_zero`, `SkewPolynomial.monomial_zero_one`, `SkewPolynomial.monomial_zero_right`, `SkewPolynomial.support_add`, `SkewPolynomial.support_eq_empty`, `SkewPolynomial.monomial_mul_monomial`, `SkewPolynomial.instSMulCommClass`, `SkewPolynomial.instIsScalarTower`, `SkewPolynomial.smul_monomial`

---

← Back to Index