Structures · Algebra
StrongRankCondition
We say that R satisfies the strong rank condition if (Fin n → R) →ₗ[R] (Fin m → R) injective
implies n ≤ m.
- Shape
- One type argument · adds le_of_fin_injective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by288
- Module.finrank_pos
- Module.finrank_eq_card_basis
- Module.finrank_eq_rank
- Module.finrank_mul_finrank
- Module.finrank_self
- Module.Basis.mk_eq_rank''
- Module.rank_lt_aleph0
- Module.finBasis
- Module.finrank_eq_card_chooseBasisIndex
- Submodule.finrank_le
- Module.rank_self
- Module.finrank_fintype_fun_eq_card
- PowerBasis.finrank
- Submodule.finrank_quotient_add_finrank
- Submodule.finrank_mono
- Module.Basis.mk_eq_rank
- Module.Free.rank_eq_card_chooseBasisIndex
- rank_span_le
- Submodule.finrank_eq_zero
- Module.finrank_pos_iff
- Module.finrank_eq_zero_of_subsingleton
- Module.finite_of_finrank_pos
- finrank_span_le_card
- rank_eq_card_basis
- Module.finrank_of_not_finite
- rank_mul_rank
- Module.rank_lt_aleph0_iff
- finrank_span_eq_card
- rank_span
- rank_fun'
- Module.finBasisOfFinrankEq
- Module.finrank_tensorProduct
- Module.finrank_zero_iff
- Module.finrank_pi_fintype
- rank_pi
- Matrix.rank_mul_le_left
- Module.finrank_eq_nat_card_basis
- Subalgebra.bot_eq_top_iff_finrank_eq_one
- Module.finrank_fin_fun
- Module.basisUnique
- Module.finrank_pi
- Module.finrank_prod
- LinearIndependent.fintype_card_le_finrank
- sigPos_isGreatest
- Module.nonempty_linearEquiv_iff_rank_eq
- finrank_span_set_eq_card
- LinearEquiv.ofFinrankEq
- Module.finrank_top_le_finrank_of_isScalarTower
- rank_finsupp
- linearIndependent_le_basis
Ancestors0
No ancestors.