Documentation Verification Report

TensorProduct

📁 Source: Mathlib/LinearAlgebra/Span/TensorProduct.lean

Statistics

Metric	Count
Definitions `tensorEquivSpan`, `tensorSpanEquivSpan`, `tensorToSpan`	3
Theorems `coe_tensorSpanEquivSpan_apply_tmul`, `finrank_span_eq_finrank`, `finrank_span_eq_finrank_span`, `injective_tensorToSpan`, `surjective_tensorToSpan`, `tensorEquivSpan_apply_tmul`, `tensorToSpan_apply_tmul`	7
Total	10

Submodule

Definitions

Name	Category	Theorems
`tensorEquivSpan` 📖	CompOp	1 math math: `tensorEquivSpan_apply_tmul`
`tensorSpanEquivSpan` 📖	CompOp	1 math math: `coe_tensorSpanEquivSpan_apply_tmul`
`tensorToSpan` 📖	CompOp	3 math math: `surjective_tensorToSpan`, `injective_tensorToSpan`, `tensorToSpan_apply_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_tensorSpanEquivSpan_apply_tmul` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `span` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `Algebra.toModule` `module` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorSpanEquivSpan` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`finrank_span_eq_finrank` 📖	mathematical	—	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `span` `SetLike.coe` `addCommMonoid` `module`	—	`subsingleton_or_nontrivial` `Module.finrank_subsingleton` `Algebra.subsingleton` `Algebra.to_smulCommClass` `Module.finrank_eq_card_basis` `commRing_strongRankCondition`
`finrank_span_eq_finrank_span` 📖	mathematical	—	`Module.finrank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `span` `addCommMonoid` `module`	—	`span_span_of_tower` `finrank_span_eq_finrank` `Module.free_of_finite_type_torsion_free'` `Ideal.instIsTorsionFreeSubtypeMemSubmodule`
`injective_tensorToSpan` 📖	mathematical	—	`TensorProduct` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `Algebra.toModule` `module` `span` `SetLike.coe` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `tensorToSpan`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `isScalarTower'` `IsScalarTower.left` `smulCommClass_self` `IsScalarTower.to_smulCommClass` `RingHomCompTriple.ids` `LinearMap.IsScalarTower.compatibleSMul` `Algebra.injective_lift_lsmul` `Module.Flat.lTensor_preserves_injective_linearMap` `injective_inclusionSpan` `TensorProduct.isScalarTower_left` `TensorProduct.AlgebraTensorModule.curry_injective` `LinearMap.ext` `LinearMap.coe_restrictScalars` `LinearMap.coe_comp`
`surjective_tensorToSpan` 📖	mathematical	—	`TensorProduct` `Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `addCommMonoid` `Algebra.toModule` `module` `span` `SetLike.coe` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `tensorToSpan`	—	`Algebra.to_smulCommClass` `Finsupp.mem_span_iff_linearCombination` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `subtype_apply`
`tensorEquivSpan_apply_tmul` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `span` `SetLike.coe` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `Algebra.toModule` `module` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorEquivSpan` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `Algebra.to_smulCommClass`
`tensorToSpan_apply_tmul` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `setLike` `span` `SetLike.coe` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `addCommMonoid` `Algebra.toModule` `module` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `LinearMap.instFunLike` `tensorToSpan` `TensorProduct.tmul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Algebra.to_smulCommClass`

---

← Back to Index