Depth

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

Statistics

Metric	Count
Definitions	0
Theorems linearMap_subsingleton_of_mem_annihilator, subsingleton_linearMap_iff	2
Total	2

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearMap_subsingleton_of_mem_annihilator 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.annihilator	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid	—	LinearMap.ext smul_zero map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Module.mem_annihilator map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass
subsingleton_linearMap_iff 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Module.annihilator IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	subsingleton_or_nontrivial Submodule.zero_mem zero associatedPrimes.nonempty Ideal.subset_union_prime_finite associatedPrimes.finite IsAssociatedPrime.isPrime biUnion_associatedPrimes_eq_compl_regular Mathlib.Tactic.Push.not_and_eq Module.mem_support_iff_of_finite IsScalarTower.left Localization.AtPrime.isLocalRing Submodule.Quotient.nontrivial_iff Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator PrimeSpectrum.isPrime Module.mem_support_iff Module.Finite.instLocalizationLocalizedModule IsLocalRing.maximalIdeal_le_jacobson Ideal.instIsTwoSided_1 isAssociatedPrime_iff IsLocalization.instIsNoetherianRingLocalization AssociatedPrimes.mem_iff Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes Module.Projective.of_free Module.Free.of_divisionRing exists_ne LinearMap.map_smul RingHomCompTriple.ids le_of_eq LinearMap.ker_eq_bot Submodule.ker_liftQ_eq_bot LinearMap.ext Submodule.Quotient.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Module.finitePresentation_of_finite Mathlib.Tactic.Contrapose.contrapose₄ smulCommClass_self RingHomInvPair.ids IsScalarTower.right IsScalarTower.to_smulCommClass' OreLocalization.instIsScalarTower_1 LinearMap.instIsScalarTower LinearEquiv.map_eq_zero_iff Subsingleton.eq_zero LocalizedModule.instSubsingleton linearMap_subsingleton_of_mem_annihilator

---

← Back to Index