Documentation Verification Report

VertexOperator

📁 Source: Mathlib/Algebra/Vertex/VertexOperator.lean

Statistics

Metric	Count
Definitions `VertexOperator`, `ncoeff`, `of_coeff`, `«term_[[_]]»`	4
Theorems `coeff_eq_ncoeff`, `coeff_eq_zero_of_lt_order`, `ext`, `ext_iff`, `ncoeff_add`, `ncoeff_apply`, `ncoeff_eq_zero_of_lt_order`, `ncoeff_of_coeff`, `ncoeff_smul`, `of_coeff_apply_coeff`	10
Total	14

VertexOperator

Definitions

Name	Category	Theorems
`ncoeff` 📖	CompOp	4 math math: `ncoeff_apply`, `ncoeff_of_coeff`, `ncoeff_eq_zero_of_lt_order`, `coeff_eq_ncoeff`
`of_coeff` 📖	CompOp	2 math math: `of_coeff_apply_coeff`, `ncoeff_of_coeff`
`«term_[[_]]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_ncoeff` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HVertexOperator` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `LinearMap.addCommMonoid` `HahnModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `Pi.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.Function.module` `LinearMap.instFunLike` `HVertexOperator.coeff` `VertexOperator` `Module.End` `ncoeff`	—	`smulCommClass_self` `ncoeff_apply` `neg_sub` `add_sub_cancel_left`
`coeff_eq_zero_of_lt_order` 📖	mathematical	`HahnSeries.order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `HahnModule.of` `VertexOperator` `LinearMap.instFunLike` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `RingHom.id` `Semiring.toNonAssocSemiring`	`LinearMap` `HVertexOperator` `LinearMap.addCommMonoid` `Pi.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.Function.module` `HVertexOperator.coeff`	—	`smulCommClass_self` `coeff_eq_ncoeff` `ncoeff_eq_zero_of_lt_order`
`ext` 📖	—	`DFunLike.coe` `VertexOperator` `HahnModule` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—	`LinearMap.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `VertexOperator` `HahnModule` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`ext`
`ncoeff_add` 📖	mathematical	—	`DFunLike.coe`	—	`map_add`
`ncoeff_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `VertexOperator` `LinearMap.addCommMonoid` `HahnModule` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `Pi.addCommMonoid` `Module.End` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.Function.module` `LinearMap.instFunLike` `ncoeff` `HVertexOperator` `HVertexOperator.coeff`	—	`smulCommClass_self`
`ncoeff_eq_zero_of_lt_order` 📖	mathematical	`HahnSeries.order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `HahnModule.of` `VertexOperator` `LinearMap.instFunLike` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `RingHom.id` `Semiring.toNonAssocSemiring`	`Module.End` `LinearMap` `LinearMap.addCommMonoid` `Pi.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.Function.module` `ncoeff`	—	`smulCommClass_self` `HahnSeries.coeff_eq_zero_of_lt_order`
`ncoeff_of_coeff` 📖	mathematical	`BddBelow` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring`	`LinearMap` `VertexOperator` `LinearMap.addCommMonoid` `HahnModule` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `Pi.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Pi.Function.module` `ncoeff` `of_coeff`	—	`LinearMap.ext` `smulCommClass_self` `ncoeff_apply` `HVertexOperator.coeff_apply_apply` `of_coeff_apply_coeff`
`ncoeff_smul` 📖	mathematical	—	`DFunLike.coe`	—	`map_smul`
`of_coeff_apply_coeff` 📖	mathematical	`BddBelow` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring`	`HahnSeries.coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `HahnModule.of` `VertexOperator` `HahnModule.instAddCommMonoid` `HahnModule.instBaseModule` `of_coeff`	—	—

(root)

Definitions

Name	Category	Theorems
`VertexOperator` 📖	CompOp	5 math math: `VertexOperator.of_coeff_apply_coeff`, `VertexOperator.ncoeff_apply`, `VertexOperator.ext_iff`, `VertexOperator.ncoeff_of_coeff`, `VertexOperator.coeff_eq_ncoeff`

---

← Back to Index