Stability

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

Statistics

Metric	Count
Definitions	0
Theorems baseChange, isBaseChange, localizedModule, of_isLocalizedModule, trans	5
Total	5

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	—	Module.Flat TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	Algebra.to_smulCommClass instTensorProduct IsScalarTower.right of_free Module.Free.self
isBaseChange 📖	mathematical	IsBaseChange	Module.Flat	—	of_linearEquiv Algebra.to_smulCommClass baseChange RingHomInvPair.ids
localizedModule 📖	mathematical	—	Module.Flat Localization CommSemiring.toCommMonoid LocalizedModule OreLocalization.instCommSemiring OreLocalization.oreSetComm OreLocalization.instAddCommMonoidOreLocalization MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction OreLocalization.instModule	—	isBaseChange IsScalarTower.left IsScalarTower.right OreLocalization.instIsScalarTower_1 isLocalizedModule_iff_isBaseChange Localization.isLocalization localizedModuleIsLocalizedModule
of_isLocalizedModule 📖	mathematical	—	Module.Flat	—	isBaseChange isLocalizedModule_iff_isBaseChange
trans 📖	mathematical	—	Module.Flat	—	iff_lTensor_injectiveₛ IsScalarTower.to_smulCommClass smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' TensorProduct.AlgebraTensorModule.coe_lTensor Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.left EquivLike.injective_comp LinearEquiv.coe_coe RingHomCompTriple.ids LinearMap.coe_comp IsScalarTower.right TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange EquivLike.comp_injective lTensor_preserves_injective_linearMap Subtype.val_injective

---

← Back to Index