Basic

📁 Source: Mathlib/RingTheory/Flat/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems includeLeft_injective, includeRight_injective, nontrivial_of_algebraMap_injective_of_flat_left, nontrivial_of_algebraMap_injective_of_flat_right, tensorProduct_of_flat_of_forall_fg, of_flat, of_flat_of_isBaseChange, map_id_injective_of_flat_left, map_id_injective_of_flat_right, map_injective_of_flat_left_right, map_injective_of_flat_right_left, tmul_of_flat_left, tmul_of_flat_right, rTensor_injective_iff_subtype, rTensor_injective_of_fg, dfinsupp, dfinsupp_iff, directSum, directSum_iff, equiv_iff, finsupp, iff_lTensor_exact, iff_lTensor_exact', iff_lTensor_injectiveₛ, iff_lTensor_preserves_injective_linearMap, iff_lTensor_preserves_injective_linearMap', iff_lTensor_preserves_injective_linearMapₛ, iff_rTensor_exact, iff_rTensor_exact', iff_rTensor_injectiveₛ, iff_rTensor_preserves_injective_linearMap, iff_rTensor_preserves_injective_linearMap', iff_rTensor_preserves_injective_linearMapₛ, instSubalgebraToSubmodule, instTensorProduct, lTensor_exact, lTensor_preserves_injective_linearMap, linearIndependent_one_tmul, of_free, of_linearEquiv, of_projective, of_retract, of_shrink, of_ulift, out, rTensor_exact, rTensor_preserves_injective_linearMap, self, shrink, tensorProduct_mapIncl_injective_of_left, tensorProduct_mapIncl_injective_of_right, ulift, flat_iff, tmul_of_flat_left, tmul_of_flat_right, map_injective_of_flat_flat, map_injective_of_flat_flat', nontrivial_of_linearMap_injective_of_flat_left, nontrivial_of_linearMap_injective_of_flat_right	59
Total	59

Algebra.TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
includeLeft_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe AlgHom instSemiring leftAlgebra AlgHom.funLike includeLeft	—	RingHomInvPair.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Module.Flat.lTensor_preserves_injective_linearMap LinearEquiv.injective
includeRight_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe AlgHom instSemiring instAlgebra AlgHom.funLike includeRight	—	RingHomInvPair.ids map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Module.Flat.rTensor_preserves_injective_linearMap LinearEquiv.injective
nontrivial_of_algebraMap_injective_of_flat_left 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Nontrivial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	TensorProduct.nontrivial_of_linearMap_injective_of_flat_left
nontrivial_of_algebraMap_injective_of_flat_right 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	Nontrivial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	TensorProduct.nontrivial_of_linearMap_injective_of_flat_right

IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensorProduct_of_flat_of_forall_fg 📖	mathematical	IsReduced TensorProduct Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Subalgebra.toSemiring Algebra.toModule Subalgebra.instModuleSubtypeMem instZeroTensorProduct Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring Subalgebra.algebra	IsReduced TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instZeroTensorProduct Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring	—	exists_isNilpotent_of_not_isReduced Algebra.to_smulCommClass exists_fg_and_mem_baseChange IsScalarTower.to_smulCommClass IsScalarTower.right Module.Flat.lTensor_preserves_injective_linearMap Subtype.val_injective IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_flat 📖	mathematical	IsSMulRegular Algebra.toSMul CommSemiring.toSemiring Algebra.id	IsSMulRegular Algebra.toSMul CommSemiring.toSemiring Algebra.id DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	of_flat_of_isBaseChange IsScalarTower.right IsBaseChange.linearMap
of_flat_of_isBaseChange 📖	mathematical	IsBaseChange IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	smulCommClass_self IsTensorProduct.map_id_injective_of_flat_left LinearMap.IsScalarTower.compatibleSMul IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap

IsTensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_id_injective_of_flat_left 📖	mathematical	IsTensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike map LinearMap.id	—	smulCommClass_self RingHomInvPair.ids inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_eq equiv_symm_apply map_add SemilinearMapClass.toAddHomClass EquivLike.toEmbeddingLike Module.Flat.lTensor_preserves_injective_linearMap
map_id_injective_of_flat_right 📖	mathematical	IsTensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike map LinearMap.id	—	smulCommClass_self RingHomInvPair.ids inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_eq equiv_symm_apply map_add SemilinearMapClass.toAddHomClass EquivLike.toEmbeddingLike Module.Flat.rTensor_preserves_injective_linearMap
map_injective_of_flat_left_right 📖	mathematical	IsTensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike map	—	smulCommClass_self RingHomInvPair.ids inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_eq equiv_symm_apply map_add SemilinearMapClass.toAddHomClass EquivLike.toEmbeddingLike TensorProduct.map_injective_of_flat_flat'
map_injective_of_flat_right_left 📖	mathematical	IsTensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike map	—	smulCommClass_self RingHomInvPair.ids inductionOn map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_eq equiv_symm_apply map_add SemilinearMapClass.toAddHomClass EquivLike.toEmbeddingLike TensorProduct.map_injective_of_flat_flat

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul_of_flat_left 📖	mathematical	LinearIndependent CommSemiring.toSemiring	LinearIndependent TensorProduct TensorProduct.tmul CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule	—	eq_1 RingHomInvPair.ids LinearEquiv.coe_toLinearMap RingHomCompTriple.ids LinearMap.coe_comp Finsupp.lhom_ext' LinearMap.ext_ring Finsupp.linearCombination_single one_smul finsuppTensorFinsupp'_symm_single_eq_single_one_tmul TensorProduct.map_injective_of_flat_flat Module.Flat.finsupp LinearEquiv.injective
tmul_of_flat_right 📖	mathematical	LinearIndependent CommSemiring.toSemiring	LinearIndependent TensorProduct TensorProduct.tmul CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule	—	comp RingHomInvPair.ids LinearMap.linearIndependent_iff_of_injOn Function.Injective.injOn LinearEquiv.injective tmul_of_flat_left Function.Bijective.injective Prod.swap_bijective

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rTensor_injective_iff_subtype 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instFunLike	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule instFunLike rTensor Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids Submodule.addCommMonoid Submodule.module Submodule.subtype	—	RingHomInvPair.ids RingHomSurjective.ids RingHomCompTriple.ids RingHomSurjective.invPair LinearEquiv.injective EquivLike.injective_comp EquivLike.comp_injective
rTensor_injective_of_fg 📖	mathematical	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule instFunLike rTensor restrict	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule instFunLike rTensor	—	RingHomSurjective.ids Submodule.exists_fg_le_subset_range_rTensor_subtype Submodule.FG.exists_rTensor_fg_inclusion_eq Submodule.FG.map RingHomCompTriple.ids rTensor_comp_apply Submodule.map_le_iff_le_comap

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat_iff 📖	mathematical	—	Flat TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	—	—

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dfinsupp 📖	mathematical	Module.Flat	Module.Flat DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module CommSemiring.toSemiring	—	dfinsupp_iff
dfinsupp_iff 📖	mathematical	—	Module.Flat DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.addCommMonoid DFinsupp.module CommSemiring.toSemiring	—	directSum_iff
directSum 📖	mathematical	Module.Flat	Module.Flat DirectSum instAddCommMonoidDirectSum DirectSum.instModule CommSemiring.toSemiring	—	directSum_iff
directSum_iff 📖	mathematical	—	Module.Flat DirectSum instAddCommMonoidDirectSum DirectSum.instModule CommSemiring.toSemiring	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left EquivLike.comp_injective RingHomCompTriple.ids TensorProduct.directSumRight_comp_rTensor
equiv_iff 📖	mathematical	—	Module.Flat	—	RingHomInvPair.ids of_linearEquiv
finsupp 📖	mathematical	—	Module.Flat Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule	—	of_linearEquiv directSum self
iff_lTensor_exact 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Function.Exact TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor instZeroTensorProduct	—	iff_lTensor_exact' UnivLE.small univLE_of_max UnivLE.self
iff_lTensor_exact' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Function.Exact TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor instZeroTensorProduct	—	lTensor_exact iff_lTensor_preserves_injective_linearMap' LinearMap.ker_eq_bot eq_bot_iff LinearMap.lTensor_zero LinearMap.map_eq_zero_iff
iff_lTensor_injectiveₛ 📖	mathematical	—	Module.Flat TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor Submodule.subtype	—	—
iff_lTensor_preserves_injective_linearMap 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor	—	iff_lTensor_preserves_injective_linearMap' UnivLE.small univLE_of_max UnivLE.self
iff_lTensor_preserves_injective_linearMap' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor	—	—
iff_lTensor_preserves_injective_linearMapₛ 📖	mathematical	—	Module.Flat TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor	—	—
iff_rTensor_exact 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Function.Exact TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor instZeroTensorProduct	—	iff_rTensor_exact' UnivLE.small univLE_of_max UnivLE.self
iff_rTensor_exact' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Function.Exact TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor instZeroTensorProduct	—	rTensor_exact iff_rTensor_preserves_injective_linearMap' LinearMap.ker_eq_bot eq_bot_iff LinearMap.rTensor_zero LinearMap.map_eq_zero_iff
iff_rTensor_injectiveₛ 📖	mathematical	—	Module.Flat TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	—	rTensor_preserves_injective_linearMap Subtype.val_injective
iff_rTensor_preserves_injective_linearMap 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	iff_rTensor_preserves_injective_linearMap' UnivLE.small univLE_of_max UnivLE.self
iff_rTensor_preserves_injective_linearMap' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	rTensor_preserves_injective_linearMap iff_rTensor_preserves_injective_linearMapₛ
iff_rTensor_preserves_injective_linearMapₛ 📖	mathematical	—	Module.Flat TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	rTensor_preserves_injective_linearMap Module.Finite.small RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids LinearMap.rTensor_injective_iff_subtype Subtype.val_injective
instSubalgebraToSubmodule 📖	mathematical	—	Module.Flat Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership Submodule.setLike DFunLike.coe OrderEmbedding Subalgebra Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Submodule.addCommMonoid Submodule.module	—	—
instTensorProduct 📖	mathematical	—	Module.Flat TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule CommSemiring.toSemiring IsScalarTower.to_smulCommClass	—	IsScalarTower.to_smulCommClass iff_rTensor_injectiveₛ RestrictScalars.isScalarTower IsScalarTower.to_smulCommClass' Submodule.isScalarTower' TensorProduct.isScalarTower RingHomInvPair.ids smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.left RingHomCompTriple.ids TensorProduct.AlgebraTensorModule.rTensor_tensor EquivLike.toEmbeddingLike rTensor_preserves_injective_linearMap LinearMap.IsScalarTower.compatibleSMul Submodule.injective_subtype
lTensor_exact 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Function.Exact TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor instZeroTensorProduct	—	RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids LinearMap.exact_iff lTensor_exact Quotient.mk''_surjective LinearMap.lTensor_comp Function.Exact.comp_injective lTensor_preserves_injective_linearMap Subtype.val_injective map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
lTensor_preserves_injective_linearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor	—	rTensor_preserves_injective_linearMap
linearIndependent_one_tmul 📖	mathematical	LinearIndependent CommSemiring.toSemiring	LinearIndependent TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	Algebra.to_smulCommClass LinearIndependent.eq_1 LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' TensorProduct.isScalarTower_left IsScalarTower.right LinearMap.coe_restrictScalars RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left Finsupp.linearCombination_one_tmul lTensor_preserves_injective_linearMap
of_free 📖	mathematical	—	Module.Flat	—	of_projective Module.Projective.of_free
of_linearEquiv 📖	mathematical	—	Module.Flat	—	RingHomInvPair.ids of_retract RingHomCompTriple.ids LinearEquiv.self_trans_symm
of_projective 📖	mathematical	—	Module.Flat	—	RingHomCompTriple.ids Module.projective_def' of_retract finsupp
of_retract 📖	mathematical	LinearMap.comp CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	Module.Flat	—	RingHomCompTriple.ids iff_rTensor_injectiveₛ Function.Injective.of_comp LinearMap.coe_comp LinearMap.lTensor_comp_rTensor LinearMap.rTensor_comp_lTensor Function.RightInverse.injective LinearMap.lTensor_id
of_shrink 📖	mathematical	—	Module.Flat	—	of_linearEquiv RingHomInvPair.ids
of_ulift 📖	mathematical	—	Module.Flat	—	of_linearEquiv RingHomInvPair.ids
out 📖	mathematical	Submodule.FG CommSemiring.toSemiring	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	—	—
rTensor_exact 📖	mathematical	Function.Exact DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Function.Exact TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor instZeroTensorProduct	—	RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids LinearMap.exact_iff rTensor_exact Quotient.mk''_surjective LinearMap.rTensor_comp Function.Exact.comp_injective rTensor_preserves_injective_linearMap Subtype.val_injective map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
rTensor_preserves_injective_linearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	LinearMap.rTensor_injective_of_fg Module.Finite.small UnivLE.small univLE_of_max UnivLE.self Module.Finite.iff_fg RingHomInvPair.ids Module.Finite.equiv RingHomSurjective.ids RingHomCompTriple.ids LinearMap.rTensor_injective_iff_subtype Module.flat_iff Module.Finite.range
self 📖	mathematical	—	Module.Flat NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	RingHomInvPair.ids Equiv.injective_comp Equiv.comp_injective one_smul Subtype.coe_injective
shrink 📖	mathematical	—	Module.Flat Shrink Shrink.instAddCommMonoid Shrink.instModule CommSemiring.toSemiring	—	of_linearEquiv
tensorProduct_mapIncl_injective_of_left 📖	mathematical	—	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.mapIncl	—	TensorProduct.map_injective_of_flat_flat' Submodule.subtype_injective
tensorProduct_mapIncl_injective_of_right 📖	mathematical	—	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.mapIncl	—	TensorProduct.map_injective_of_flat_flat Submodule.subtype_injective
ulift 📖	mathematical	—	Module.Flat ULift.addCommMonoid ULift.module' CommSemiring.toSemiring	—	of_linearEquiv

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_injective_of_flat_flat 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule LinearMap.instFunLike map	—	RingHomCompTriple.ids LinearMap.lTensor_comp_rTensor Module.Flat.lTensor_preserves_injective_linearMap Module.Flat.rTensor_preserves_injective_linearMap
map_injective_of_flat_flat' 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule LinearMap.instFunLike map	—	RingHomCompTriple.ids LinearMap.rTensor_comp_lTensor Module.Flat.rTensor_preserves_injective_linearMap Module.Flat.lTensor_preserves_injective_linearMap
nontrivial_of_linearMap_injective_of_flat_left 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike	Nontrivial TensorProduct	—	Function.Injective.nontrivial RingHomInvPair.ids Module.Flat.lTensor_preserves_injective_linearMap LinearEquiv.injective
nontrivial_of_linearMap_injective_of_flat_right 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike	Nontrivial TensorProduct	—	Function.Injective.nontrivial RingHomInvPair.ids Module.Flat.rTensor_preserves_injective_linearMap LinearEquiv.injective

TensorProduct.LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tmul_of_flat_left 📖	mathematical	LinearIndepOn CommSemiring.toSemiring	LinearIndepOn TensorProduct TensorProduct.tmul CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule SProd.sprod Set Set.instSProd	—	LinearIndependent.comp LinearIndependent.tmul_of_flat_left Equiv.injective
tmul_of_flat_right 📖	mathematical	LinearIndepOn CommSemiring.toSemiring	LinearIndepOn TensorProduct TensorProduct.tmul CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule SProd.sprod Set Set.instSProd	—	LinearIndependent.comp LinearIndependent.tmul_of_flat_right Equiv.injective

---

← Back to Index