Documentation Verification Report

Vanishing

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

Statistics

Metric	Count
Definitions `VanishesTrivially`	1
Theorems `vanishesTrivially_comp`, `of_fintype`, `forall_vanishesTrivially_iff_forall_fg_rTensor_injective`, `forall_vanishesTrivially_iff_forall_rTensor_injective`, `rTensor_injective_of_forall_fg_rTensor_injective`, `rTensor_injective_of_forall_vanishesTrivially`, `sum_tmul_eq_zero_of_vanishesTrivially`, `vanishesTrivially_iff_sum_tmul_eq_zero`, `vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective`, `vanishesTrivially_of_sum_tmul_eq_zero`, `vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective`	11
Total	12

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vanishesTrivially_comp` 📖	mathematical	—	`TensorProduct.VanishesTrivially` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`Finset.sum_congr` `forall_congr_right` `sum_comp` `exists_congr_right` `symm_apply_apply`

TensorProduct

Definitions

Name	Category	Theorems
`VanishesTrivially` 📖	MathDef	9 math math: `forall_vanishesTrivially_iff_forall_fg_rTensor_injective`, `vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective`, `Equiv.vanishesTrivially_comp`, `vanishesTrivially_of_sum_tmul_eq_zero`, `forall_vanishesTrivially_iff_forall_rTensor_injective`, `Module.isTrivialRelation_iff_vanishesTrivially`, `VanishesTrivially.of_fintype`, `vanishesTrivially_iff_sum_tmul_eq_zero`, `vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_vanishesTrivially_iff_forall_fg_rTensor_injective` 📖	mathematical	—	`VanishesTrivially` `Fin.fintype` `TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	—	`rTensor_injective_of_forall_vanishesTrivially` `vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective` `Submodule.fg_span` `Set.finite_range` `Finite.of_fintype`
`forall_vanishesTrivially_iff_forall_rTensor_injective` 📖	mathematical	—	`VanishesTrivially` `Fin.fintype` `TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	—	`rTensor_injective_of_forall_vanishesTrivially` `vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective`
`rTensor_injective_of_forall_fg_rTensor_injective` 📖	mathematical	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	—	`forall_vanishesTrivially_iff_forall_rTensor_injective` `forall_vanishesTrivially_iff_forall_fg_rTensor_injective`
`rTensor_injective_of_forall_vanishesTrivially` 📖	mathematical	`VanishesTrivially` `Fin.fintype`	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `exists_finset` `Finset.sum_attach` `sum_tmul_eq_zero_of_vanishesTrivially` `Equiv.sum_comp` `Finset.sum_coe_sort` `map_sum` `Finset.sum_congr` `Equiv.vanishesTrivially_comp` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `injective_iff_map_eq_zero'` `Submodule.injective_subtype`
`sum_tmul_eq_zero_of_vanishesTrivially` 📖	mathematical	`VanishesTrivially`	`Finset.sum` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `Finset.univ` `tmul` `instZeroTensorProduct`	—	`Finset.sum_congr` `tmul_sum` `smulCommClass_self` `tmul_smul` `CompatibleSMul.isScalarTower` `IsScalarTower.left` `Finset.sum_comm` `zero_tmul` `Finset.sum_const_zero`
`vanishesTrivially_iff_sum_tmul_eq_zero` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`VanishesTrivially` `Finset.sum` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `Finset.univ` `tmul` `instZeroTensorProduct`	—	`sum_tmul_eq_zero_of_vanishesTrivially` `vanishesTrivially_of_sum_tmul_eq_zero`
`vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective` 📖	mathematical	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype`	`VanishesTrivially` `Finset.sum` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `Finset.univ` `tmul` `instZeroTensorProduct`	—	`sum_tmul_eq_zero_of_vanishesTrivially` `vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective`
`vanishesTrivially_of_sum_tmul_eq_zero` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `Finset.sum` `TensorProduct` `addCommMonoid` `Finset.univ` `tmul` `instZeroTensorProduct`	`VanishesTrivially`	—	`Finsupp.linearCombination_single` `one_smul` `RingHomSurjective.ids` `LinearMap.range_eq_top` `top_le_iff` `Submodule.span_le` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `LinearMap.exact_subtype_ker_map` `rTensor_exact` `Function.Exact.linearMap_ker_eq` `exists_finset` `VanishesTrivially.of_fintype` `Finset.sum_attach` `zero_smul` `RingHomInvPair.ids` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `finsuppScalarLeft_apply_tmul` `Finsupp.sum_single_index` `Finsupp.single_zero` `Finsupp.finset_sum_apply` `Finsupp.single_apply` `Finset.sum_ite_eq'` `Finsupp.sum_apply` `Finsupp.sum_ite_eq'` `Finsupp.sum_fintype` `LinearMap.mem_ker`
`vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective` 📖	mathematical	`TensorProduct` `CommRing.toCommSemiring` `Submodule` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `Submodule.subtype` `Finset.sum` `Finset.univ` `tmul` `instZeroTensorProduct`	`VanishesTrivially`	—	`Submodule.subset_span` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.injective_subtype` `Submodule.map_span` `Submodule.map_top` `Submodule.range_subtype` `Submodule.coe_subtype` `Set.range_comp` `Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `vanishesTrivially_of_sum_tmul_eq_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `injective_iff_map_eq_zero'`

TensorProduct.VanishesTrivially

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_fintype` 📖	mathematical	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`TensorProduct.VanishesTrivially`	—	`Finset.sum_congr` `Equiv.sum_comp` `Equiv.forall_congr_right`

---

← Back to Index