Structures · Algebra
RankCondition
We say that R satisfies the rank condition if (Fin n → R) →ₗ[R] (Fin m → R) surjective
implies m ≤ n.
- Shape
- One type argument · adds le_of_fin_surjective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- le_of_fin_surjective
- RankCondition.le_of_fin_surjective
- card_le_of_surjective
- card_le_of_surjective'
- Module.Basis.le_span
- Submodule.spanRank_span_range_of_linearIndependent
- Basis.le_span''
- Module.Finite.exists_nat_not_surjective
- basis_le_span'
- Module.Basis.mk_eq_spanRank
- Submodule.spanRank_span_of_linearIndepOn
- instRankConditionMulOpposite
- invariantBasisNumber_of_rankCondition
Ancestors0
No ancestors.