Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `map_smul_top_ne_top_iff_of_faithfullyFlat`, `directSum`, `finsupp`, `iff_exact_iff_lTensor_exact`, `iff_exact_iff_rTensor_exact`, `iff_flat_and_ideal_smul_eq_top`, `iff_flat_and_lTensor_faithful`, `iff_flat_and_lTensor_reflects_triviality`, `iff_flat_and_proper_ideal`, `iff_flat_and_rTensor_faithful`, `iff_flat_and_rTensor_reflects_triviality`, `iff_zero_iff_lTensor_zero`, `iff_zero_iff_rTensor_zero`, `instOfNontrivialOfFree`, `instTensorProduct`, `lTensor_bijective_iff_bijective`, `lTensor_exact_iff_exact`, `lTensor_injective_iff_injective`, `lTensor_nontrivial`, `lTensor_reflects_exact`, `lTensor_reflects_triviality`, `lTensor_surjective_iff_surjective`, `nontrivial_tensorProduct_iff_left`, `nontrivial_tensorProduct_iff_right`, `of_linearEquiv`, `one_tmul_eq_zero_iff`, `rTensor_exact_iff_exact`, `rTensor_nontrivial`, `rTensor_reflects_exact`, `rTensor_reflects_triviality`, `range_le_ker_of_exact_rTensor`, `self`, `submodule_ne_top`, `subsingleton_tensorProduct_iff_left`, `subsingleton_tensorProduct_iff_right`, `toFlat`, `trans`, `zero_iff_lTensor_zero`, `zero_iff_rTensor_zero`, `iff_flat_tensorProduct`, `of_flat_tensorProduct`, `faithfullyFlat_iff`	42
Total	42

IsBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul_top_ne_top_iff_of_faithfullyFlat` 📖	—	`IsBaseChange` `AddCommGroup.toAddCommMonoid` `CommRing.toCommSemiring`	—	—	`IsScalarTower.left` `Iff.not` `Submodule.Quotient.subsingleton_iff` `Equiv.subsingleton_congr` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `IsScalarTower.to_smulCommClass` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `TensorProduct.isScalarTower_left` `Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfullyFlat_iff` 📖	mathematical	—	`FaithfullyFlat` `Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsScalarTower.left`

Module.FaithfullyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directSum` 📖	mathematical	`Module.FaithfullyFlat`	`DirectSum` `AddCommGroup.toAddCommMonoid` `DirectSum.instAddCommGroup` `DirectSum.instModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`iff_flat_and_lTensor_faithful` `Module.Flat.directSum` `toFlat` `Nontrivial.exists_pair_ne` `lTensor_nontrivial` `Equiv.nontrivial` `DirectSum.instSMulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `RingHomInvPair.ids` `DirectSum.of_injective`
`finsupp` 📖	mathematical	—	`Module.FaithfullyFlat` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Finsupp.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule`	—	`of_linearEquiv` `directSum` `self`
`iff_exact_iff_lTensor_exact` 📖	mathematical	—	`Module.FaithfullyFlat` `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`	—	—
`iff_exact_iff_rTensor_exact` 📖	mathematical	—	`Module.FaithfullyFlat` `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`	—	`rTensor_exact_iff_exact` `iff_flat_and_rTensor_reflects_triviality` `Module.Flat.iff_rTensor_exact` `LinearMap.rTensor_zero`
`iff_flat_and_ideal_smul_eq_top` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Top.top` `Ideal` `CommSemiring.toSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsScalarTower.left` `iff_flat_and_proper_ideal`
`iff_flat_and_lTensor_faithful` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Nontrivial` `TensorProduct`	—	`iff_flat_and_rTensor_faithful` `Equiv.nontrivial` `RingHomInvPair.ids`
`iff_flat_and_lTensor_reflects_triviality` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`iff_flat_and_lTensor_faithful`
`iff_flat_and_proper_ideal` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsScalarTower.left` `Module.faithfullyFlat_iff` `Ideal.exists_le_maximal` `eq_top_iff` `Submodule.smul_mono` `Ideal.IsMaximal.ne_top`
`iff_flat_and_rTensor_faithful` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Nontrivial` `TensorProduct`	—	`toFlat` `rTensor_nontrivial` `IsScalarTower.left` `Equiv.nontrivial` `RingHomInvPair.ids` `ULift.nontrivial` `IsDomain.toNontrivial` `Ideal.instIsTwoSided_1` `Ideal.Quotient.isDomain` `Ideal.IsMaximal.isPrime'` `not_subsingleton` `Submodule.Quotient.subsingleton_iff`
`iff_flat_and_rTensor_reflects_triviality` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`iff_flat_and_rTensor_faithful`
`iff_zero_iff_lTensor_zero` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.lTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instZero`	—	`toFlat` `zero_iff_lTensor_zero` `iff_flat_and_lTensor_reflects_triviality` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`iff_zero_iff_rTensor_zero` 📖	mathematical	—	`Module.FaithfullyFlat` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.rTensor` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instZero`	—	`toFlat` `zero_iff_rTensor_zero` `iff_flat_and_rTensor_reflects_triviality` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`instOfNontrivialOfFree` 📖	mathematical	—	`Module.FaithfullyFlat`	—	`of_linearEquiv` `finsupp` `Module.Free.instNonemptyChooseBasisIndexOfNontrivial`
`instTensorProduct` 📖	mathematical	—	`Module.FaithfullyFlat` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `iff_flat_and_rTensor_reflects_triviality` `Module.Flat.baseChange` `toFlat` `IsScalarTower.of_algebraMap_smul` `Equiv.subsingleton` `RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `smulCommClass_self` `IsScalarTower.left` `rTensor_reflects_triviality`
`lTensor_bijective_iff_bijective` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	—
`lTensor_exact_iff_exact` 📖	mathematical	—	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor` `TensorProduct.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lTensor_reflects_exact` `Module.Flat.lTensor_exact` `toFlat`
`lTensor_injective_iff_injective` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`LinearMap.exact_zero_iff_injective` `lTensor_exact_iff_exact` `LinearMap.lTensor_zero`
`lTensor_nontrivial` 📖	mathematical	—	`Nontrivial` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Equiv.nontrivial` `RingHomInvPair.ids` `rTensor_nontrivial`
`lTensor_reflects_exact` 📖	mathematical	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor` `TensorProduct.zero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`rTensor_reflects_exact` `Function.Exact.of_ladder_linearEquiv_of_exact` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext` `IsScalarTower.to_smulCommClass`
`lTensor_reflects_triviality` 📖	—	—	—	—	`rTensor_reflects_triviality` `Function.Injective.subsingleton` `RingHomInvPair.ids` `Equiv.injective`
`lTensor_surjective_iff_surjective` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor`	—	`LinearMap.exact_zero_iff_surjective` `lTensor_exact_iff_exact` `LinearMap.lTensor_zero`
`nontrivial_tensorProduct_iff_left` 📖	mathematical	—	`Nontrivial` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `subsingleton_tensorProduct_iff_left`
`nontrivial_tensorProduct_iff_right` 📖	mathematical	—	`Nontrivial` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `subsingleton_tensorProduct_iff_right`
`of_linearEquiv` 📖	mathematical	—	`Module.FaithfullyFlat`	—	`RingHomInvPair.ids` `iff_flat_and_lTensor_faithful` `Module.Flat.of_linearEquiv` `toFlat` `Equiv.nontrivial` `lTensor_nontrivial`
`one_tmul_eq_zero_iff` 📖	mathematical	—	`TensorProduct.tmul` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `TensorProduct` `TensorProduct.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`SMulCommClass.symm` `smulCommClass_self` `zero_iff_lTensor_zero` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearMap.ext_ring` `one_smul` `mul_one` `smul_eq_mul` `Algebra.to_smulCommClass` `TensorProduct.smul_tmul'` `smul_zero` `DFunLike.congr_fun` `TensorProduct.tmul_zero`
`rTensor_exact_iff_exact` 📖	mathematical	—	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `TensorProduct.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`rTensor_reflects_exact` `Module.Flat.rTensor_exact` `toFlat`
`rTensor_nontrivial` 📖	mathematical	—	`Nontrivial` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`nontrivial_iff_exists_ne` `one_smul` `Submodule.mem_annihilator_span_singleton` `Ideal.eq_top_iff_one` `SMulCommClass.symm` `smulCommClass_self` `LinearMap.ker_eq_bot` `eq_bot_iff` `Quotient.inductionOn'` `IsScalarTower.left` `iff_flat_and_proper_ideal` `subsingleton_or_nontrivial` `Submodule.Quotient.subsingleton_iff` `Function.Injective.subsingleton` `RingHomInvPair.ids` `Module.Flat.rTensor_preserves_injective_linearMap` `toFlat` `LinearEquiv.injective`
`rTensor_reflects_exact` 📖	mathematical	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `TensorProduct.zero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `LinearMap.exact_iff` `range_le_ker_of_exact_rTensor` `RingHomInvPair.ids` `Equiv.subsingleton_congr` `Submodule.Quotient.subsingleton_iff` `LinearMap.range_eq_top` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `TensorProduct.zero_tmul` `RingHomCompTriple.ids` `Module.Flat.rTensor_preserves_injective_linearMap` `toFlat` `Subtype.val_injective` `LinearMap.mem_range_self` `LinearMap.comp_codRestrict` `LinearMap.comp_apply` `LinearMap.rTensor_def` `LinearMap.rTensor_comp` `LinearMap.comp_assoc` `RingHomCompTriple.right_ids` `LinearMap.subtype_comp_codRestrict` `Submodule.subtype_comp_inclusion` `map_add` `SemilinearMapClass.toAddHomClass` `rTensor_reflects_triviality` `le_antisymm` `Submodule.comap_subtype_eq_top` `Submodule.range_inclusion`
`rTensor_reflects_triviality` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `rTensor_nontrivial`
`range_le_ker_of_exact_rTensor` 📖	mathematical	`Function.Exact` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.rTensor` `TensorProduct.zero`	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHomSurjective.ids` `LinearMap.ker`	—	`RingHomSurjective.ids` `LinearMap.mem_ker` `Submodule.mem_span_singleton_self` `Subtype.coe_ne_coe` `Function.Exact.apply_apply_eq_zero` `Submodule.ext` `Submodule.mem_span_set` `TensorProduct.span_tmul_eq_top` `Submodule.mem_span_singleton` `IsScalarTower.left` `Finset.sum_eq_zero` `Module.Flat.rTensor_preserves_injective_linearMap` `toFlat` `Submodule.injective_subtype` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `Submodule.isScalarTower'` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.rTensor_tmul` `Submodule.subtype_apply` `smul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `not_subsingleton_iff_nontrivial` `rTensor_reflects_triviality`
`self` 📖	mathematical	—	`Module.FaithfullyFlat` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Module.Flat.of_free` `Module.Free.self` `IsScalarTower.left` `Iff.not` `Ideal.eq_top_iff_one` `Ideal.IsMaximal.ne_top` `IsScalarTower.right` `Ideal.mul_top` `Ideal.instIsTwoSided_1`
`submodule_ne_top` 📖	—	—	—	—	—
`subsingleton_tensorProduct_iff_left` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`rTensor_reflects_triviality` `Unique.instSubsingleton`
`subsingleton_tensorProduct_iff_right` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`lTensor_reflects_triviality` `Unique.instSubsingleton`
`toFlat` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—
`trans` 📖	mathematical	—	`Module.FaithfullyFlat`	—	`iff_zero_iff_lTensor_zero` `Module.Flat.trans` `toFlat` `zero_iff_lTensor_zero` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `Algebra.to_smulCommClass` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass'` `LinearMap.ext_ring` `LinearEquiv.injective` `smulCommClass_self` `RingHomInvPair.ids` `one_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.lTensor_zero`
`zero_iff_lTensor_zero` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `LinearMap.lTensor` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`LinearMap.lTensor_zero` `lTensor_reflects_exact` `RingHomSurjective.ids` `LinearMap.exact_iff` `LinearMap.range_zero` `LinearMap.ker_eq_bot` `Module.Flat.lTensor_preserves_injective_linearMap` `toFlat` `LinearMap.ext`
`zero_iff_rTensor_zero` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `LinearMap.rTensor` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule`	—	`zero_iff_lTensor_zero` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `LinearEquiv.injective` `RingHomInvPair.ids` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_flat_tensorProduct` 📖	mathematical	—	`Module.Flat` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass` `of_flat_tensorProduct` `baseChange`
`of_flat_tensorProduct` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.to_smulCommClass` `iff_lTensor_preserves_injective_linearMap` `trans` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.lTensor_injective_iff_injective` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.left` `TensorProduct.isScalarTower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `EquivLike.toEmbeddingLike` `lTensor_preserves_injective_linearMap`

---

← Back to Index