Documentation Verification Report

InvariantForm

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

Statistics

Metric	Count
Definitions `orthogonal`, `lieInvariant`, `InvariantForm`	3
Theorems `atomistic`, `isSemisimple_of_nondegenerate`, `mem_orthogonal`, `orthogonal_carrier`, `orthogonal_disjoint`, `orthogonal_isCompl`, `orthogonal_isCompl_toSubmodule`, `orthogonal_toSubmodule`, `restrict_nondegenerate`, `restrict_orthogonal_nondegenerate`, `lieInvariant_iff`	11
Total	14

LieAlgebra.InvariantForm

Definitions

Name	Category	Theorems
`orthogonal` 📖	CompOp	7 math math: `orthogonal_disjoint`, `orthogonal_carrier`, `orthogonal_isCompl`, `restrict_orthogonal_nondegenerate`, `mem_orthogonal`, `orthogonal_isCompl_toSubmodule`, `orthogonal_toSubmodule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atomistic` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass`	`SupSet.sSup` `LieIdeal` `LieSubmodule.instSupSet` `setOf` `IsAtom` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `le_antisymm` `sSup_le` `LE.le.trans` `Eq.le` `bot_le` `IsAtomic.eq_bot_or_exists_atom_le` `LieSubmodule.instIsAtomicOfIsArtinian` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Codisjoint.eq_top` `IsCompl.codisjoint` `orthogonal_isCompl` `sup_inf_assoc_of_le` `LieSubmodule.instIsModularLattice` `top_inf_eq` `le_refl` `sup_le` `le_sSup` `Submodule.finrank_lt_finrank_of_lt` `FiniteDimensional.finiteDimensional_submodule` `eq_bot_iff` `orthogonal_disjoint` `le_rfl` `sSup_le_sSup`
`isSemisimple_of_nondegenerate` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass`	`LieAlgebra.IsSemisimple`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `atomistic` `Disjoint.mono_right` `orthogonal_disjoint` `sSup_le` `lie_eq_self_of_isAtom_of_nonabelian` `LieSubmodule.lieIdeal_oper_eq_span` `LieSubmodule.lieSpan_le` `orthogonal_carrier` `LinearMap.BilinForm.isOrtho_def` `neg_eq_zero` `LieSubmodule.mem_bot` `Disjoint.eq_bot` `IsAtom.disjoint_of_ne` `LieSubmodule.lie_le_inf` `LieSubmodule.lie_mem_lie` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`mem_orthogonal` 📖	mathematical	`LinearMap.BilinForm.lieInvariant`	`LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `orthogonal` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.BilinForm` `LinearMap.addCommMonoid` `LinearMap.module` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`orthogonal_carrier` 📖	mathematical	`LinearMap.BilinForm.lieInvariant`	`SetLike.coe` `LieSubmodule` `LieSubmodule.instSetLike` `orthogonal` `setOf`	—	—
`orthogonal_disjoint` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`Disjoint` `orthogonal`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `disjoint_iff` `IsAtom.lt_iff` `lt_iff_le_and_ne` `eq_bot_iff` `lie_eq_self_of_isAtom_of_nonabelian` `LieSubmodule.lieIdeal_oper_eq_span` `LieSubmodule.lieSpan_le` `neg_eq_zero` `lie_mem_left`
`orthogonal_isCompl` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`IsCompl` `orthogonal`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.isCompl_toSubmodule` `orthogonal_isCompl_toSubmodule`
`orthogonal_isCompl_toSubmodule` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`IsCompl` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPartialOrder` `Submodule.completeLattice` `LieSubmodule.toSubmodule` `orthogonal`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `orthogonal_toSubmodule` `LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint` `LieSubmodule.disjoint_toSubmodule` `orthogonal_disjoint`
`orthogonal_toSubmodule` 📖	mathematical	`LinearMap.BilinForm.lieInvariant`	`LieSubmodule.toSubmodule` `orthogonal` `LinearMap.BilinForm.orthogonal` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—
`restrict_nondegenerate` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`Submodule` `CommSemiring.toSemiring` `Submodule.setLike` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.BilinForm.restrict`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal` `orthogonal_isCompl_toSubmodule`
`restrict_orthogonal_nondegenerate` 📖	mathematical	`LinearMap.BilinForm.Nondegenerate` `Semifield.toCommSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.BilinForm.lieInvariant` `lieRingSelfModule` `LinearMap.BilinForm.IsRefl` `IsLieAbelian` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `IsAtom` `LieIdeal` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `LieSubmodule.instCompleteLattice`	`Submodule` `CommSemiring.toSemiring` `Submodule.setLike` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `orthogonal` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.BilinForm.restrict`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal` `LinearMap.BilinForm.orthogonal_orthogonal` `IsCompl.symm` `orthogonal_isCompl_toSubmodule`

LinearMap.BilinForm

Definitions

Name	Category	Theorems
`lieInvariant` 📖	MathDef	2 math math: `lieInvariant_iff`, `LieModule.traceForm_lieInvariant`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lieInvariant_iff` 📖	mathematical	—	`lieInvariant` `LinearMap.BilinForm` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieSubmodule` `LinearMap.addCommGroup` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LinearMap.module` `LinearMap.addCommMonoid` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `LinearMap.instSMulCommClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instLieRingModule` `Module.Dual.instLieRingModule` `Module.Dual.instLieModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieModule.maxTrivSubmodule` `LinearMap.instLieModule`	—	`Algebra.to_smulCommClass` `LinearMap.instSMulCommClass` `Module.Dual.instLieModule` `LinearMap.instLieModule` `ext` `LieHom.lie_apply` `LinearMap.sub_apply` `Module.Dual.lie_apply` `LinearMap.zero_apply` `sub_self` `LinearMap.congr_fun₂`

RootPairing

Definitions

Name	Category	Theorems
`InvariantForm` 📖	CompData	—

---

← Back to Index