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 Algebra.toModule 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 Algebra.toModule 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 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 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 📖	—	IsReduced TensorProduct Subalgebra SetLike.instMembership Subalgebra.instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Subalgebra.toSemiring Algebra.toModule Subalgebra.instModuleSubtypeMem TensorProduct.zero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring Subalgebra.algebra	—	—	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	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	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	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	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	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	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	TensorProduct TensorProduct.tmul 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	TensorProduct TensorProduct.tmul 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 TensorProduct.addCommMonoid TensorProduct.instModule 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 📖	—	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	—	—	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	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	DirectSum instAddCommMonoidDirectSum DirectSum.instModule CommSemiring.toSemiring	—	directSum_iff
directSum_iff 📖	mathematical	—	Module.Flat DirectSum instAddCommMonoidDirectSum DirectSum.instModule CommSemiring.toSemiring	—	RingHomInvPair.ids 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 TensorProduct.zero	—	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 TensorProduct.zero	—	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 TensorProduct.zero	—	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 TensorProduct.zero	—	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' IsScalarTower.left TensorProduct.isScalarTower RingHomInvPair.ids smulCommClass_self TensorProduct.smulCommClass_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	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.lTensor TensorProduct.zero	—	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 TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.lTensor	—	rTensor_preserves_injective_linearMap
linearIndependent_one_tmul 📖	mathematical	LinearIndependent CommSemiring.toSemiring	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 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	TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.rTensor TensorProduct.zero	—	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 TensorProduct.addCommMonoid TensorProduct.instModule 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 addCommMonoid instModule 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 addCommMonoid instModule 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	TensorProduct TensorProduct.tmul 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	TensorProduct TensorProduct.tmul TensorProduct.addCommMonoid TensorProduct.instModule SProd.sprod Set Set.instSProd	—	LinearIndependent.comp LinearIndependent.tmul_of_flat_right Equiv.injective

---

← Back to Index