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 RingHom.id	—	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 AssociatePrimes.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