Documentation Verification Report

SkewAdjoint

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

Statistics

Metric	Count
Definitions `skewAdjointLieSubalgebra`, `skewAdjointLieSubalgebraEquiv`, `skewAdjointMatricesLieSubalgebra`, `skewAdjointMatricesLieSubalgebraEquiv`, `skewAdjointMatricesLieSubalgebraEquivTranspose`	5
Theorems `isSkewAdjoint_bracket`, `isSkewAdjoint_bracket`, `lie_transpose`, `mem_skewAdjointMatricesLieSubalgebra`, `mem_skewAdjointMatricesLieSubalgebra_unit_smul`, `skewAdjointLieSubalgebraEquiv_apply`, `skewAdjointLieSubalgebraEquiv_symm_apply`, `skewAdjointMatricesLieSubalgebraEquivTranspose_apply`, `skewAdjointMatricesLieSubalgebraEquiv_apply`	9
Total	14

LinearMap.BilinForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSkewAdjoint_bracket` 📖	mathematical	`Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `LinearMap.addCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `LinearMap.skewAdjointSubmodule` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `Semiring.toModule`	`Bracket.bracket` `LieRingModule.toBracket` `Module.End.instRing` `LinearMap.addCommGroup` `LinearMap.instLieRingModule` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.End.instLieRingModule` `Module.End.instLieModule`	—	`smulCommClass_self` `IsScalarTower.left` `Module.End.instLieModule` `LinearMap.mem_skewAdjointSubmodule` `neg_mul_neg` `LinearMap.IsAdjointPair.comp` `neg_sub` `LinearMap.IsAdjointPair.sub`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSkewAdjoint_bracket` 📖	mathematical	`Matrix` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `skewAdjointMatricesSubmodule`	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.ofAssociativeRing` `instRing` `CommRing.toRing` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`lie_transpose` `LieRing.of_associative_ring_bracket` `sub_mul` `mul_assoc` `mul_neg` `neg_mul` `sub_eq_add_neg` `mul_add` `Distrib.leftDistribClass` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`lie_transpose` 📖	mathematical	—	`transpose` `Bracket.bracket` `Matrix` `LieRingModule.toBracket` `LieRing.ofAssociativeRing` `instRing` `CommRing.toRing` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	`transpose_sub` `transpose_mul`

(root)

Definitions

Name	Category	Theorems
`skewAdjointLieSubalgebra` 📖	CompOp	2 math math: `skewAdjointLieSubalgebraEquiv_apply`, `skewAdjointLieSubalgebraEquiv_symm_apply`
`skewAdjointLieSubalgebraEquiv` 📖	CompOp	2 math math: `skewAdjointLieSubalgebraEquiv_apply`, `skewAdjointLieSubalgebraEquiv_symm_apply`
`skewAdjointMatricesLieSubalgebra` 📖	CompOp	4 math math: `skewAdjointMatricesLieSubalgebraEquivTranspose_apply`, `mem_skewAdjointMatricesLieSubalgebra`, `mem_skewAdjointMatricesLieSubalgebra_unit_smul`, `skewAdjointMatricesLieSubalgebraEquiv_apply`
`skewAdjointMatricesLieSubalgebraEquiv` 📖	CompOp	1 math math: `skewAdjointMatricesLieSubalgebraEquiv_apply`
`skewAdjointMatricesLieSubalgebraEquivTranspose` 📖	CompOp	1 math math: `skewAdjointMatricesLieSubalgebraEquivTranspose_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_skewAdjointMatricesLieSubalgebra` 📖	mathematical	—	`Matrix` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointMatricesLieSubalgebra` `Submodule` `CommSemiring.toSemiring` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Matrix.module` `Semiring.toModule` `Submodule.setLike` `skewAdjointMatricesSubmodule`	—	—
`mem_skewAdjointMatricesLieSubalgebra_unit_smul` 📖	mathematical	—	`Matrix` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointMatricesLieSubalgebra` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Units.instSMul` `Matrix.smul` `Algebra.toSMul`	—	`mul_neg` `Matrix.mul_smul` `Units.smulCommClass_left` `Algebra.to_smulCommClass` `inv_smul_smul` `Matrix.smul_mul` `Units.instIsScalarTower` `IsScalarTower.right` `smul_neg`
`skewAdjointLieSubalgebraEquiv_apply` 📖	mathematical	—	`Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieSubalgebra` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointLieSubalgebra` `DFunLike.coe` `LieEquiv` `LinearMap.compl₁₂` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `skewAdjointLieSubalgebraEquiv` `LinearEquiv.lieConj`	—	`RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left`
`skewAdjointLieSubalgebraEquiv_symm_apply` 📖	mathematical	—	`Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieSubalgebra` `LieRing.ofAssociativeRing` `Module.End.instRing` `LieAlgebra.ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointLieSubalgebra` `LinearMap.compl₁₂` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `LinearEquiv.toLinearMap` `RingHom.id` `RingHomInvPair.ids` `DFunLike.coe` `LieEquiv` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `LieEquiv.symm` `skewAdjointLieSubalgebraEquiv` `LinearEquiv.lieConj` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left`
`skewAdjointMatricesLieSubalgebraEquivTranspose_apply` 📖	mathematical	`Matrix.transpose` `DFunLike.coe` `AlgEquiv` `Matrix` `CommRing.toCommSemiring` `Matrix.semiring` `CommSemiring.toSemiring` `Matrix.instAlgebra` `Algebra.id` `AlgEquiv.instFunLike`	`LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Ring.toSemiring` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointMatricesLieSubalgebra` `LieEquiv` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `skewAdjointMatricesLieSubalgebraEquivTranspose`	—	—
`skewAdjointMatricesLieSubalgebraEquiv_apply` 📖	mathematical	—	`Matrix` `LieSubalgebra` `LieRing.ofAssociativeRing` `Matrix.instRing` `CommRing.toRing` `LieAlgebra.ofAssociativeAlgebra` `Matrix.instAlgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `Algebra.id` `SetLike.instMembership` `LieSubalgebra.instSetLike` `skewAdjointMatricesLieSubalgebra` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.transpose` `DFunLike.coe` `LieEquiv` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `EquivLike.toFunLike` `LieEquiv.instEquivLike` `skewAdjointMatricesLieSubalgebraEquiv` `Matrix.inv`	—	`Matrix.lieConj_symm_apply`

---

← Back to Index