Flat

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

Statistics

Metric	Count
Definitions	0
Theorems of_faithfullyFlat, of_faithfullyFlat_of_isBaseChange, isRegular_of_isLocalization_of_mem, isRegular_of_isLocalizedModule_of_mem, of_flat, of_flat_of_isBaseChange, of_isLocalization, of_isLocalizedModule	8
Total	8

RingTheory.Sequence.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfullyFlat 📖	mathematical	RingTheory.Sequence.IsRegular Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	of_faithfullyFlat_of_isBaseChange IsScalarTower.right IsBaseChange.linearMap
of_faithfullyFlat_of_isBaseChange 📖	mathematical	IsBaseChange AddCommGroup.toAddCommMonoid CommRing.toCommSemiring RingTheory.Sequence.IsRegular	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange Module.FaithfullyFlat.toFlat toIsWeaklyRegular IsScalarTower.left Ideal.map_ofList IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat top_ne_smul

RingTheory.Sequence.IsWeaklyRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRegular_of_isLocalization_of_mem 📖	mathematical	RingTheory.Sequence.IsWeaklyRegular Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	RingTheory.Sequence.IsRegular DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	IsLocalization.AtPrime.nontrivial isRegular_of_isLocalizedModule_of_mem IsScalarTower.right Module.Finite.self instIsLocalizedModuleLinearMapOfIsLocalization
isRegular_of_isLocalizedModule_of_mem 📖	mathematical	RingTheory.Sequence.IsWeaklyRegular Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	RingTheory.Sequence.IsRegular DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	IsLocalization.AtPrime.isLocalRing IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal IsLocalization.AtPrime.to_map_mem_maximal_iff of_isLocalizedModule
of_flat 📖	mathematical	RingTheory.Sequence.IsWeaklyRegular Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	of_flat_of_isBaseChange IsScalarTower.right IsBaseChange.linearMap
of_flat_of_isBaseChange 📖	mathematical	IsBaseChange AddCommGroup.toAddCommMonoid CommRing.toCommSemiring RingTheory.Sequence.IsWeaklyRegular	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	RingHomInvPair.ids Algebra.to_smulCommClass RingHomCompTriple.ids Submodule.Quotient.isScalarTower LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.smulCommClass_left smulCommClass_self IsBaseChange.of_equiv IsSMulRegular.of_flat_of_isBaseChange
of_isLocalization 📖	mathematical	RingTheory.Sequence.IsWeaklyRegular Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	of_isLocalizedModule IsScalarTower.right instIsLocalizedModuleLinearMapOfIsLocalization
of_isLocalizedModule 📖	mathematical	RingTheory.Sequence.IsWeaklyRegular	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.flat of_flat_of_isBaseChange IsLocalizedModule.isBaseChange

---

← Back to Index