Documentation Verification Report

BaseChange

📁 Source: Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Statistics

Metric	Count
Definitions `IsBalanced`, `restrictScalars`, `restrictScalars'`, `restrictScalarsRat`	4
Theorems `isPerfectCompl`, `instIsBalancedOfIsRootSystem`, `instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars'`, `restrictScalars_coe_coroot`, `restrictScalars_coe_root`, `restrictScalars_pairing`, `restrictScalars_toLinearMap_apply_apply`	7
Total	11

RootPairing

Definitions

Name	Category	Theorems
`IsBalanced` 📖	CompData	2 math math: `instIsBalanced`, `instIsBalancedOfIsRootSystem`
`restrictScalars` 📖	CompOp	—
`restrictScalars'` 📖	CompOp	5 math math: `instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars'`, `restrictScalars_coe_coroot`, `restrictScalars_pairing`, `restrictScalars_coe_root`, `restrictScalars_toLinearMap_apply_apply`
`restrictScalarsRat` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsBalancedOfIsRootSystem` 📖	mathematical	—	`IsBalanced`	—	`isPerfPair_toLinearMap` `Algebra.to_smulCommClass` `LinearMap.IsPerfectCompl.congr_simp` `IsRootSystem.span_root_eq_top` `IsRootSystem.span_coroot_eq_top`
`instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars'` 📖	mathematical	—	`IsRootSystem` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `coroot` `Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.module` `restrictScalars'`	—	`Submodule.span_setOf_mem_eq_top` `Set.ext`
`restrictScalars_coe_coroot` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `coroot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `root` `Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.module` `restrictScalars'`	—	—
`restrictScalars_coe_root` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `coroot` `Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.module` `restrictScalars'`	—	—
`restrictScalars_pairing` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `pairing` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `coroot` `Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.module` `restrictScalars'`	—	`Algebra.to_smulCommClass` `restrictScalars_toLinearMap_apply_apply`
`restrictScalars_toLinearMap_apply_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `LinearMap` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `RingHom.id` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Function.Embedding` `Function.instFunLikeEmbedding` `coroot` `Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submodule.module` `Semiring.toModule` `LinearMap.instFunLike` `root` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `toLinearMap` `restrictScalars'`	—	`Algebra.to_smulCommClass` `LinearMap.restrictScalarsField_apply_apply`

RootPairing.IsBalanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPerfectCompl` 📖	mathematical	—	`LinearMap.IsPerfectCompl` `RootPairing.toLinearMap` `RootPairing.isPerfPair_toLinearMap` `RootPairing.rootSpan` `RootPairing.corootSpan`	—	—

---

← Back to Index