Documentation Verification Report

VectorSpace

📁 Source: Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

Statistics

Metric	Count
Definitions `basis`, `basis`, `basisSingleOne`	3
Theorems `instFree`, `equivFun_symm_single`, `linearIndependent_single`, `linearIndependent_single_iff`, `sum_single_ite`, `basisSingleOne_repr`, `basis_repr`, `coe_basis`, `coe_basisSingleOne`, `isCompl_range_lmapDomain_span`, `lcomapDomain_eq_linearProjOfIsCompl`, `linearIndependent_single`, `linearIndependent_single_iff`, `linearIndependent_single_of_ne_zero`, `linearIndependent_single_one`, `instFreeInt`, `repr_smul'`, `dfinsupp`, `finsupp`, `trans`, `instFree`, `instFree`	22
Total	25

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFree` 📖	mathematical	—	`Module.Free` `AddMonoidAlgebra` `addAddCommMonoid` `module`	—	`Module.Free.finsupp`

Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFun_symm_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `Module.Basis.equivFun` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.Basis` `Module.Basis.instFunLike`	—	`nonempty_fintype` `RingHomInvPair.ids` `Finite.of_fintype` `Module.Basis.equivFun_symm_apply` `Finset.sum_congr` `Pi.single_apply` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq'`

DFinsupp

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_single` 📖	mathematical	`LinearIndependent`	`DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single` `addCommMonoid` `module`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `ext` `Finsupp.linearCombination_single` `one_smul` `single_apply` `sigmaFinsuppEquivDFinsupp_single` `mapRange_single` `LinearIndependent.eq_1` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mapRange_injective` `Equiv.injective`
`linearIndependent_single_iff` 📖	mathematical	—	`LinearIndependent` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single` `addCommMonoid` `module`	—	`LinearIndependent.of_comp` `LinearIndependent.comp` `sigma_mk_injective` `linearIndependent_single`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_single_ite` 📖	mathematical	—	`sum` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `univ` `Finsupp.single`	—	`sum_congr` `Finsupp.single_zero` `sum_ite_eq` `mem_univ`

Finsupp

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	2 math math: `basis_repr`, `coe_basis`
`basisSingleOne` 📖	CompOp	2 math math: `coe_basisSingleOne`, `basisSingleOne_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basisSingleOne_repr` 📖	mathematical	—	`Module.Basis.repr` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `basisSingleOne` `LinearEquiv.refl`	—	`RingHomInvPair.ids`
`basis_repr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `basis`	—	`RingHomInvPair.ids`
`coe_basis` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `Module.Basis.instFunLike` `basis` `single`	—	`RingHomInvPair.ids` `Module.Basis.apply_eq_iff` `ext` `single_eq_same` `Module.Basis.repr_self` `single_apply_left` `sigma_mk_injective` `single_eq_of_ne'` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`coe_basisSingleOne` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `Module.Basis.instFunLike` `basisSingleOne` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids` `Module.Basis.apply_eq_iff`
`isCompl_range_lmapDomain_span` 📖	mathematical	`IsCompl` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder` `Set.range`	`Submodule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `module` `Semiring.toModule` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `RingHomSurjective.ids` `lmapDomain` `Submodule.span` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomSurjective.ids` `range_lmapDomain` `LinearIndependent.isCompl_span_image` `Module.Basis.linearIndependent` `Module.Basis.span_eq` `Set.range_comp`
`lcomapDomain_eq_linearProjOfIsCompl` 📖	mathematical	`IsCompl` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder` `Set.range`	`lcomapDomain` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Semiring.toModule` `LinearMap.linearProjOfIsCompl` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instAddCommGroup` `Ring.toAddCommGroup` `module` `Submodule.span` `AddCommGroup.toAddCommMonoid` `single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `lmapDomain` `mapDomain_injective` `isCompl_range_lmapDomain_span`	—	`Module.Basis.ext` `mapDomain_injective` `isCompl_range_lmapDomain_span` `codisjoint_iff` `IsCompl.codisjoint` `mapDomain_single` `coe_basisSingleOne` `comapDomain_single` `LinearMap.linearProjOfIsCompl_apply_left` `LinearMap.linearProjOfIsCompl_apply_right'` `Submodule.subset_span` `ext` `single_apply` `Set.disjoint_range_iff` `IsCompl.disjoint`
`linearIndependent_single` 📖	mathematical	`LinearIndependent`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single` `instAddCommMonoid` `module`	—	`RingHomInvPair.ids` `DFinsupp.toFinsupp_single` `LinearIndependent.map_injOn` `DFinsupp.linearIndependent_single` `Function.Injective.injOn` `LinearEquiv.injective`
`linearIndependent_single_iff` 📖	mathematical	—	`LinearIndependent` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `single` `instAddCommMonoid` `module`	—	`LinearIndependent.of_comp` `LinearIndependent.comp` `sigma_mk_injective` `linearIndependent_single`
`linearIndependent_single_of_ne_zero` 📖	mathematical	—	`LinearIndependent` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `single` `Ring.toSemiring` `instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `module`	—	`linearIndependent_equiv` `linearIndependent_single`
`linearIndependent_single_one` 📖	mathematical	—	`LinearIndependent` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule`	—	`Module.Basis.linearIndependent`

FreeAbelianGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFreeInt` 📖	mathematical	—	`Module.Free` `FreeAbelianGroup` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `AddCommGroup.toIntModule`	—	—

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`repr_smul'` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingHomInvPair.ids` `smul_eq_mul` `algebraMap_smul` `IsScalarTower.right` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finsupp.smul_apply`

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dfinsupp` 📖	mathematical	`Module.Free`	`DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.addCommMonoid` `DFinsupp.module`	—	`of_basis`
`finsupp` 📖	mathematical	—	`Module.Free` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module`	—	`of_basis`
`trans` 📖	mathematical	—	`Module.Free` `CommSemiring.toSemiring`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearMap.CompatibleSMul.finsupp_cod` `LinearMap.IsScalarTower.compatibleSMul` `IsScalarTower.right` `of_equiv` `finsupp` `self`

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFree` 📖	mathematical	—	`Module.Free` `MonoidAlgebra` `addCommMonoid` `module`	—	`Module.Free.finsupp`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFree` 📖	mathematical	—	`Module.Free` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule`	—	`Module.Free.of_equiv` `AddMonoidAlgebra.instFree` `Module.Free.self` `RingHomInvPair.ids`

---

← Back to Index