SemiDirect

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

Statistics

Metric	Count
Definitions `SemiDirectSum`, `inl`, `inr`, `inst`, `instAddCommGroup`, `instBracket`, `instLieRing`, `instModule`, `left`, `prod_iso`, `projl`, `projr`, `right`, `toProd`, `toProdl`, `«term_⋊⁅_⁆_»`	16
Theorems `add_eq_mk`, `ext`, `ext_iff`, `inl_eq_mk`, `inl_injective`, `inr_eq_mk`, `instIsExtensionInlProjr`, `lie_eq_mk`, `neg_eq_mk`, `prod_iso_invFun_left`, `prod_iso_invFun_right`, `prod_iso_toFun`, `projl_inl_apply`, `projl_inr_apply`, `projl_mk`, `projr_inl_apply`, `projr_inr_apply`, `projr_mk`, `projr_surjective`, `smul_eq_mk`, `sub_eq_mk`, `toProd_apply`, `toProdl_coe`, `zero_eq_mk`	24
Total	40

LieAlgebra

Definitions

Name	Category	Theorems
`SemiDirectSum` 📖	CompData	22 math math: `SemiDirectSum.projl_mk`, `SemiDirectSum.projr_inl_apply`, `SemiDirectSum.toProd_apply`, `SemiDirectSum.zero_eq_mk`, `SemiDirectSum.prod_iso_toFun`, `SemiDirectSum.projr_inr_apply`, `SemiDirectSum.lie_eq_mk`, `SemiDirectSum.instIsExtensionInlProjr`, `SemiDirectSum.inl_eq_mk`, `SemiDirectSum.sub_eq_mk`, `SemiDirectSum.smul_eq_mk`, `SemiDirectSum.projr_mk`, `SemiDirectSum.prod_iso_invFun_left`, `SemiDirectSum.toProdl_coe`, `SemiDirectSum.add_eq_mk`, `SemiDirectSum.neg_eq_mk`, `SemiDirectSum.prod_iso_invFun_right`, `SemiDirectSum.inl_injective`, `SemiDirectSum.projr_surjective`, `SemiDirectSum.inr_eq_mk`, `SemiDirectSum.projl_inl_apply`, `SemiDirectSum.projl_inr_apply`
`«term_⋊⁅_⁆_»` 📖	CompOp	—

LieAlgebra.SemiDirectSum

Definitions

Name	Category	Theorems
`inl` 📖	CompOp	5 math math: `projr_inl_apply`, `instIsExtensionInlProjr`, `inl_eq_mk`, `inl_injective`, `projl_inl_apply`
`inr` 📖	CompOp	3 math math: `projr_inr_apply`, `inr_eq_mk`, `projl_inr_apply`
`inst` 📖	CompOp	13 math math: `projr_inl_apply`, `prod_iso_toFun`, `projr_inr_apply`, `instIsExtensionInlProjr`, `inl_eq_mk`, `projr_mk`, `prod_iso_invFun_left`, `prod_iso_invFun_right`, `inl_injective`, `projr_surjective`, `inr_eq_mk`, `projl_inl_apply`, `projl_inr_apply`
`instAddCommGroup` 📖	CompOp	9 math math: `projl_mk`, `zero_eq_mk`, `sub_eq_mk`, `smul_eq_mk`, `toProdl_coe`, `add_eq_mk`, `neg_eq_mk`, `projl_inl_apply`, `projl_inr_apply`
`instBracket` 📖	CompOp	1 math math: `lie_eq_mk`
`instLieRing` 📖	CompOp	13 math math: `projr_inl_apply`, `prod_iso_toFun`, `projr_inr_apply`, `instIsExtensionInlProjr`, `inl_eq_mk`, `projr_mk`, `prod_iso_invFun_left`, `prod_iso_invFun_right`, `inl_injective`, `projr_surjective`, `inr_eq_mk`, `projl_inl_apply`, `projl_inr_apply`
`instModule` 📖	CompOp	5 math math: `projl_mk`, `smul_eq_mk`, `toProdl_coe`, `projl_inl_apply`, `projl_inr_apply`
`left` 📖	CompOp	10 math math: `projl_mk`, `toProd_apply`, `ext_iff`, `prod_iso_toFun`, `lie_eq_mk`, `sub_eq_mk`, `smul_eq_mk`, `prod_iso_invFun_left`, `add_eq_mk`, `neg_eq_mk`
`prod_iso` 📖	CompOp	3 math math: `prod_iso_toFun`, `prod_iso_invFun_left`, `prod_iso_invFun_right`
`projl` 📖	CompOp	3 math math: `projl_mk`, `projl_inl_apply`, `projl_inr_apply`
`projr` 📖	CompOp	5 math math: `projr_inl_apply`, `projr_inr_apply`, `instIsExtensionInlProjr`, `projr_mk`, `projr_surjective`
`right` 📖	CompOp	10 math math: `toProd_apply`, `ext_iff`, `prod_iso_toFun`, `lie_eq_mk`, `sub_eq_mk`, `smul_eq_mk`, `projr_mk`, `add_eq_mk`, `neg_eq_mk`, `prod_iso_invFun_right`
`toProd` 📖	CompOp	2 math math: `toProd_apply`, `toProdl_coe`
`toProdl` 📖	CompOp	1 math math: `toProdl_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_mk` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup` `left` `right`	—	`lieAlgebraSelfModule`
`ext` 📖	—	`left` `right`	—	—	`lieAlgebraSelfModule`
`ext_iff` 📖	mathematical	—	`left` `right`	—	`lieAlgebraSelfModule` `ext`
`inl_eq_mk` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieHom.instFunLike` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	`lieAlgebraSelfModule`
`inl_injective` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `DFunLike.coe` `LieHom` `instLieRing` `inst` `LieHom.instFunLike` `inl`	—	`lieAlgebraSelfModule`
`inr_eq_mk` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieHom.instFunLike` `inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	`lieAlgebraSelfModule`
`instIsExtensionInlProjr` 📖	mathematical	—	`LieAlgebra.IsExtension` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `inl` `projr`	—	`lieAlgebraSelfModule` `LieSubalgebra.ext`
`lie_eq_mk` 📖	mathematical	—	`Bracket.bracket` `LieAlgebra.SemiDirectSum` `instBracket` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LieRing.toAddCommGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `LieRingModule.toBracket` `lieRingSelfModule` `left` `DFunLike.coe` `LieDerivation` `LieAlgebra.toModule` `lieAlgebraSelfModule` `LieDerivation.instFunLike` `LieHom` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instFunLike` `right`	—	`lieAlgebraSelfModule`
`neg_eq_mk` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup` `left` `right`	—	`lieAlgebraSelfModule`
`prod_iso_invFun_left` 📖	mathematical	—	`left` `LieHom` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instZero` `LieEquiv.invFun` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `prod_iso`	—	`lieAlgebraSelfModule`
`prod_iso_invFun_right` 📖	mathematical	—	`right` `LieHom` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instZero` `LieEquiv.invFun` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `prod_iso`	—	`lieAlgebraSelfModule`
`prod_iso_toFun` 📖	mathematical	—	`DFunLike.coe` `LieEquiv` `LieAlgebra.SemiDirectSum` `LieHom` `LieDerivation` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `lieAlgebraSelfModule` `LieDerivation.instLieRing` `LieDerivation.instLieAlgebra` `LieHom.instZero` `instLieRing` `inst` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `prod_iso` `left` `right`	—	`lieAlgebraSelfModule`
`projl_inl_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LieAlgebra.SemiDirectSum` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup` `instModule` `LieAlgebra.toModule` `LinearMap.instFunLike` `projl` `LieHom` `instLieRing` `inst` `LieHom.instFunLike` `inl`	—	`lieAlgebraSelfModule`
`projl_inr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LieAlgebra.SemiDirectSum` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup` `instModule` `LieAlgebra.toModule` `LinearMap.instFunLike` `projl` `LieHom` `instLieRing` `inst` `LieHom.instFunLike` `inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lieAlgebraSelfModule`
`projl_mk` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LieAlgebra.SemiDirectSum` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup` `instModule` `LieAlgebra.toModule` `LinearMap.instFunLike` `projl` `left`	—	`lieAlgebraSelfModule`
`projr_inl_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieHom.instFunLike` `projr` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	`lieAlgebraSelfModule`
`projr_inr_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieHom.instFunLike` `projr` `inr`	—	`lieAlgebraSelfModule`
`projr_mk` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.SemiDirectSum` `instLieRing` `inst` `LieHom.instFunLike` `projr` `right`	—	`lieAlgebraSelfModule`
`projr_surjective` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `DFunLike.coe` `LieHom` `instLieRing` `inst` `LieHom.instFunLike` `projr`	—	`lieAlgebraSelfModule`
`smul_eq_mk` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `instModule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `left` `right`	—	`lieAlgebraSelfModule`
`sub_eq_mk` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `LieRing.toAddCommGroup` `left` `right`	—	`lieAlgebraSelfModule`
`toProd_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LieAlgebra.SemiDirectSum` `EquivLike.toFunLike` `Equiv.instEquivLike` `toProd` `left` `right`	—	`lieAlgebraSelfModule`
`toProdl_coe` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LieAlgebra.SemiDirectSum` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `Prod.instAddCommMonoid` `LieRing.toAddCommGroup` `instModule` `Prod.instModule` `LieAlgebra.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toProdl` `Equiv` `Equiv.instEquivLike` `toProd`	—	`lieAlgebraSelfModule` `RingHomInvPair.ids`
`zero_eq_mk` 📖	mathematical	—	`LieAlgebra.SemiDirectSum` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroup` `LieRing.toAddCommGroup`	—	`lieAlgebraSelfModule`

---

← Back to Index