Loop

📁 Source: Mathlib/Algebra/Lie/Loop.lean

Statistics

Metric	Count
Definitions residuePairing, toFinsupp, twoCochainOfBilinear, twoCocycleOfBilinear, loopAlgebra, loopAlgebraEquivLaurent	6
Theorems residuePairing_apply_apply, toFinsupp_single_tmul, toFinsupp_symm_single, twoCochainOfBilinear_apply_apply, twoCocycleOfBilinear_coe	5
Total	11

LieAlgebra

Definitions

Name	Category	Theorems
loopAlgebra 📖	CompOp	5 math math: LoopAlgebra.twoCochainOfBilinear_apply_apply, LoopAlgebra.toFinsupp_symm_single, LoopAlgebra.toFinsupp_single_tmul, LoopAlgebra.residuePairing_apply_apply, LoopAlgebra.twoCocycleOfBilinear_coe
loopAlgebraEquivLaurent 📖	CompOp	—

LieAlgebra.LoopAlgebra

Definitions

Name	Category	Theorems
residuePairing 📖	CompOp	2 math math: twoCochainOfBilinear_apply_apply, residuePairing_apply_apply
toFinsupp 📖	CompOp	3 math math: toFinsupp_symm_single, toFinsupp_single_tmul, residuePairing_apply_apply
twoCochainOfBilinear 📖	CompOp	2 math math: twoCochainOfBilinear_apply_apply, twoCocycleOfBilinear_coe
twoCocycleOfBilinear 📖	CompOp	1 math math: twoCocycleOfBilinear_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
residuePairing_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.loopAlgebra TensorProduct.addCommMonoid AddMonoidAlgebra AddMonoidAlgebra.addAddCommMonoid AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup AddMonoidAlgebra.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.instModule Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module residuePairing Finsupp.sum NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearEquiv Finsupp Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toFinsupp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribSMul.toSMulZeroClass LinearMap.BilinForm Finsupp.instFunLike NegZeroClass.toNeg	—	—
toFinsupp_single_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LieAlgebra.loopAlgebra Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup TensorProduct.addCommMonoid AddMonoidAlgebra AddMonoidAlgebra.addAddCommMonoid AddCommGroup.toAddCommMonoid AddMonoidAlgebra.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toFinsupp TensorProduct.tmul AddMonoidAlgebra.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finsupp.single	—	RingHomInvPair.ids LinearEquiv.apply_symm_apply
toFinsupp_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieAlgebra.loopAlgebra Finsupp.instAddCommMonoid AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid AddMonoidAlgebra AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Finsupp.module TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm toFinsupp Finsupp.single TensorProduct.tmul AddMonoidAlgebra.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids TensorProduct.equivFinsuppOfBasisLeft_symm_apply Finsupp.sum_single_index TensorProduct.tmul_zero
twoCochainOfBilinear_apply_apply 📖	mathematical	LinearMap.BilinForm.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.loopAlgebra TrivialLieModule LieAlgebra.ExtendScalars.instLieRing AddMonoidAlgebra AddMonoidAlgebra.commRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid TrivialLieModule.instAddCommGroup LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ExtendScalars.instBaseLieAlgebra TrivialLieModule.instModule LieAlgebra.ofAssociativeAlgebra LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Ring.toSemiring Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain LieModule.Cohomology.instFunLikeSubtypeLinearMapIdMemSubmoduleTwoCochain twoCochainOfBilinear LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm TrivialLieModule.equiv TensorProduct.addCommMonoid AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct.instModule Semiring.toModule LinearMap.BilinForm residuePairing AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Algebra.to_smulCommClass	—	smulCommClass_self LinearMap.instSMulCommClass
twoCocycleOfBilinear_coe 📖	mathematical	LinearMap.BilinForm.lieInvariant LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LinearMap.BilinForm.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LieAlgebra.loopAlgebra TrivialLieModule LieAlgebra.ExtendScalars.instLieRing AddMonoidAlgebra AddMonoidAlgebra.commRing NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid TrivialLieModule.instAddCommGroup LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ExtendScalars.instBaseLieAlgebra TrivialLieModule.instModule LieAlgebra.ofAssociativeAlgebra LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Ring.toSemiring Submodule LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submodule.setLike LieModule.Cohomology.twoCochain Submodule.addCommMonoid Submodule.module LieModule.Cohomology.twoCocycle TrivialLieModule.instLieRingModule TrivialLieModule.instLieModule twoCocycleOfBilinear twoCochainOfBilinear	—	smulCommClass_self LinearMap.instSMulCommClass TrivialLieModule.instLieModule

---

← Back to Index