StrongRankCondition

📁 Source: Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean

Statistics

Metric	Count
Definitions StrongRankCondition	1
Theorems commRing_strongRankCondition	1
Total	2

(root)

Definitions

Name	Category	Theorems
StrongRankCondition 📖	CompData	10 math math: IsNoetherianRing.strongRankCondition, strongRankCondition_iff_forall_not_injective, strongRankCondition_iff_forall_rank_lt_aleph0, StrongRankCondition.of_isArtinian, StrongRankCondition.of_isNoetherian, strongRankCondition_iff, strongRankCondition_of_orzechProperty, strongRankCondition_iff_forall_zero_lt_finrank, strongRankCondition_iff_succ, commRing_strongRankCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commRing_strongRankCondition 📖	mathematical	—	StrongRankCondition CommSemiring.toSemiring CommRing.toCommSemiring	—	strongRankCondition_of_orzechProperty CommRing.orzechProperty

---

← Back to Index