HVertexOperator

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

Statistics

Metric	Count
Definitions HVertexOperator, coeff, comp, compHahnSeries, of_coeff	5
Theorems coeff_add, coeff_apply_apply, coeff_comp, coeff_inj, coeff_inj_iff, coeff_isPWOsupport, coeff_of_coeff, coeff_smul, compHahnSeries_add, compHahnSeries_coeff, compHahnSeries_smul, comp_apply, ext, ext_iff, of_coeff_apply, of_coeff_coeff	16
Total	21

HVertexOperator

Definitions

Name	Category	Theorems
coeff 📖	CompOp	10 math math: VertexOperator.ncoeff_apply, of_coeff_coeff, coeff_inj_iff, coeff_inj, compHahnSeries_coeff, coeff_comp, coeff_apply_apply, VertexOperator.coeff_eq_ncoeff, VertexOperator.coeff_eq_zero_of_lt_order, coeff_of_coeff
comp 📖	CompOp	2 math math: coeff_comp, comp_apply
compHahnSeries 📖	CompOp	4 math math: compHahnSeries_smul, compHahnSeries_add, compHahnSeries_coeff, comp_apply
of_coeff 📖	CompOp	3 math math: of_coeff_coeff, of_coeff_apply, coeff_of_coeff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_add 📖	mathematical	—	DFunLike.coe	—	map_add
coeff_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike HVertexOperator 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 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 coeff HahnSeries.coeff Equiv HahnSeries EquivLike.toFunLike Equiv.instEquivLike Equiv.symm HahnModule.of	—	smulCommClass_self
coeff_comp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring HVertexOperator Lex Prod.Lex.instPartialOrder 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 coeff comp LinearMap.comp RingHomCompTriple.ids Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	smulCommClass_self
coeff_inj 📖	mathematical	—	HVertexOperator DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring 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 coeff	—	smulCommClass_self ext HahnModule.ext
coeff_inj_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring HVertexOperator 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 coeff	—	smulCommClass_self
coeff_isPWOsupport 📖	mathematical	—	Set.IsPWO PartialOrder.toPreorder Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.coeff 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 HVertexOperator LinearMap.instFunLike HahnModule.instAddCommMonoid HahnModule.instBaseModule RingHom.id Semiring.toNonAssocSemiring	—	HahnSeries.isPWO_support'
coeff_of_coeff 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	HVertexOperator LinearMap.addCommMonoid 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 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 coeff of_coeff	—	smulCommClass_self
coeff_smul 📖	mathematical	—	DFunLike.coe	—	map_smul
compHahnSeries_add 📖	mathematical	—	compHahnSeries AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid HahnSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instZero HahnSeries.instAdd HahnSeries.instAddMonoid SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid	—	HahnSeries.ext map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass HahnSeries.coeff_add
compHahnSeries_coeff 📖	mathematical	—	HahnSeries.coeff HahnSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instZero compHahnSeries DFunLike.coe HVertexOperator 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 LinearMap.instFunLike HahnModule.instAddCommMonoid HahnModule.instBaseModule RingHom.id Semiring.toNonAssocSemiring LinearMap LinearMap.addCommMonoid Pi.addCommMonoid LinearMap.module Pi.Function.module coeff	—	—
compHahnSeries_smul 📖	mathematical	—	compHahnSeries 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instZero HahnSeries.instSMul HahnSeries.instSMulZeroClass	—	HahnSeries.ext map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass HahnSeries.coeff_smul
comp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring HahnModule Lex Prod.Lex.instPartialOrder 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 LinearMap.instFunLike comp Equiv HahnSeries EquivLike.toFunLike Equiv.instEquivLike HahnModule.of HahnSeries.ofIterate compHahnSeries	—	—
ext 📖	—	DFunLike.coe HVertexOperator 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 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 HVertexOperator 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 CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid LinearMap.instFunLike HahnModule.instAddCommMonoid HahnModule.instBaseModule RingHom.id Semiring.toNonAssocSemiring	—	ext
of_coeff_apply 📖	mathematical	Set.IsPWO PartialOrder.toPreorder Function.support NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	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 HahnModule.instAddCommMonoid HahnModule.instBaseModule of_coeff Equiv HahnSeries EquivLike.toFunLike Equiv.instEquivLike HahnModule.of	—	—
of_coeff_coeff 📖	mathematical	—	of_coeff DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring HVertexOperator 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 coeff coeff_isPWOsupport	—	smulCommClass_self coeff_isPWOsupport

(root)

Definitions

Name	Category	Theorems
HVertexOperator 📖	CompOp	12 math math: HVertexOperator.coeff_isPWOsupport, VertexOperator.ncoeff_apply, HVertexOperator.of_coeff_coeff, HVertexOperator.coeff_inj_iff, HVertexOperator.coeff_inj, HVertexOperator.ext_iff, HVertexOperator.compHahnSeries_coeff, HVertexOperator.coeff_comp, HVertexOperator.coeff_apply_apply, VertexOperator.coeff_eq_ncoeff, VertexOperator.coeff_eq_zero_of_lt_order, HVertexOperator.coeff_of_coeff

---

← Back to Index