Tensor

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

Statistics

Metric	Count
Definitions	0
Theorems iff_characterModule_baer, iff_characterModule_injective, iff_lTensor_injective, iff_lTensor_injective', iff_lift_lsmul_comp_subtype_injective, iff_rTensor_injective, iff_rTensor_injective', injective_characterModule_iff_rTensor_preserves_injective_linearMap	8
Total	8

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_characterModule_baer 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Baer CommRing.toRing CharacterModule CharacterModule.instAddCommGroup CharacterModule.instModule	—	equiv_iff RingHomInvPair.ids iff_characterModule_injective UnivLE.small univLE_of_max UnivLE.self Module.Baer.iff_injective Module.Baer.congr
iff_characterModule_injective 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Injective CommRing.toRing CharacterModule CharacterModule.instAddCommGroup CharacterModule.instModule	—	injective_characterModule_iff_rTensor_preserves_injective_linearMap iff_rTensor_preserves_injective_linearMap'
iff_lTensor_injective 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor Submodule.subtype	—	RingHomInvPair.ids RingHomCompTriple.ids EquivLike.toEmbeddingLike iff_rTensor_injective
iff_lTensor_injective' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.lTensor Submodule.subtype	—	RingHomInvPair.ids RingHomCompTriple.ids EquivLike.toEmbeddingLike iff_rTensor_injective'
iff_lift_lsmul_comp_subtype_injective 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike TensorProduct.lift LinearMap.comp LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids LinearMap.lsmul Submodule.subtype	—	smulCommClass_self RingHomCompTriple.ids RingHomInvPair.ids EquivLike.toEmbeddingLike
iff_rTensor_injective 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	—	iff_rTensor_injective' injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Submodule.exists_fg_le_eq_rTensor_inclusion RingHomCompTriple.ids LinearMap.rTensor_comp_apply map_zero AddMonoidHomClass.toZeroHomClass
iff_rTensor_injective' 📖	mathematical	—	Module.Flat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor Submodule.subtype	—	smulCommClass_self
injective_characterModule_iff_rTensor_preserves_injective_linearMap 📖	mathematical	—	Module.Injective CommRing.toRing CharacterModule CharacterModule.instAddCommGroup CharacterModule.instModule TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor	—	smulCommClass_self

---

← Back to Index