Documentation Verification Report

Basis

📁 Source: Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

Statistics

Metric	Count
Definitions `tensorAlgebra`, `equivFreeAlgebra`	2
Theorems `tensorAlgebra_repr_apply`, `equivFreeAlgebra_symm_ι`, `equivFreeAlgebra_ι_apply`, `instIsDomain`, `instModuleFree`, `instNoZeroDivisors`, `rank_eq`	7
Total	9

Module.Basis

Definitions

Name	Category	Theorems
`tensorAlgebra` 📖	CompOp	1 math math: `tensorAlgebra_repr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorAlgebra_repr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorAlgebra` `Finsupp` `FreeMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringTensorAlgebra` `Finsupp.instAddCommMonoid` `Algebra.toModule` `instAlgebra` `Algebra.id` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `tensorAlgebra` `FreeAlgebra` `FreeAlgebra.instAddCommMonoid` `FreeAlgebra.instSemiring` `FreeAlgebra.instAlgebra` `FreeAlgebra.basisFreeMonoid` `AlgEquiv` `AlgEquiv.instFunLike` `TensorAlgebra.equivFreeAlgebra`	—	`RingHomInvPair.ids` `IsScalarTower.left`

TensorAlgebra

Definitions

Name	Category	Theorems
`equivFreeAlgebra` 📖	CompOp	3 math math: `equivFreeAlgebra_symm_ι`, `equivFreeAlgebra_ι_apply`, `Module.Basis.tensorAlgebra_repr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFreeAlgebra_symm_ι` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `FreeAlgebra` `TensorAlgebra` `FreeAlgebra.instSemiring` `instSemiringTensorAlgebra` `FreeAlgebra.instAlgebra` `Algebra.id` `instAlgebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivFreeAlgebra` `FreeAlgebra.ι` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `ι` `Module.Basis` `Module.Basis.instFunLike`	—	`IsScalarTower.left` `Equiv.symm_apply_eq` `equivFreeAlgebra_ι_apply`
`equivFreeAlgebra_ι_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorAlgebra` `FreeAlgebra` `instSemiringTensorAlgebra` `FreeAlgebra.instSemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `FreeAlgebra.instAlgebra` `AlgEquiv.instFunLike` `equivFreeAlgebra` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `ι` `Module.Basis` `Module.Basis.instFunLike` `FreeAlgebra.ι`	—	`IsScalarTower.left` `lift_ι_apply` `Module.Basis.repr_self` `Finsupp.linearCombination_single` `one_smul`
`instIsDomain` 📖	mathematical	—	`IsDomain` `TensorAlgebra` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instSemiringTensorAlgebra`	—	`NoZeroDivisors.to_isDomain` `instNontrivial` `IsDomain.toNontrivial` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors`
`instModuleFree` 📖	mathematical	—	`Module.Free` `TensorAlgebra` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringTensorAlgebra` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `Module.Free.exists_basis` `Module.Free.of_basis`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `TensorAlgebra` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringTensorAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`MulEquiv.noZeroDivisors` `FreeAlgebra.instNoZeroDivisors` `IsScalarTower.left`
`rank_eq` 📖	mathematical	—	`Module.rank` `TensorAlgebra` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `instSemiringTensorAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Cardinal.lift` `Cardinal.sum` `Cardinal` `Monoid.toNatPow` `Cardinal.commSemiring`	—	`IsScalarTower.left` `Module.Free.exists_basis` `LinearEquiv.rank_eq` `FreeAlgebra.rank_eq` `Cardinal.mk_list_eq_sum_pow` `Module.Basis.mk_eq_rank''` `commRing_strongRankCondition`

---

← Back to Index