Structures · Algebra
HasRankNullity
HasRankNullity.{u} is a class of rings satisfying
1. Every R-module M : Type u has a linear independent subset of cardinality Module.rank R M.
2. rank (M ⧸ N) + rank N = rank M for every R-module M : Type u and every N : Submodule R M.
Usually such a ring satisfies HasRankNullity.{w} for all universes w, and the universe
argument is there because of technical limitations to universe polymorphism.
See DivisionRing.hasRankNullity and IsDomain.hasRankNullity.
- Shape
- One type argument · adds exists_set_linearIndependent, rank_quotient_add_rank
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 by26
- Submodule.finrank_quotient_add_finrank
- Submodule.rank_quotient_add_rank
- exists_set_linearIndependent
- HasRankNullity.rank_quotient_add_rank
- LinearMap.lift_rank_range_add_rank_ker
- LinearMap.rank_eq_of_surjective
- Submodule.rank_sup_add_rank_inf_eq
- exists_linearIndependent_cons_of_lt_rank
- Submodule.disjoint_ker_of_finrank_le
- exists_linearIndependent_snoc_of_lt_rank
- exists_linearIndependent_pair_of_one_lt_rank
- HasRankNullity.exists_set_linearIndependent
- exists_linearIndepOn_of_lt_rank
- Submodule.finrank_quotient
- Submodule.rank_add_le_rank_add_rank
- LinearMap.rank_quot_submodule_map_eq
- LinearMap.rank_range_add_rank_ker
- nontrivial_of_hasRankNullity
- LinearMap.lift_rank_quot_map_le
- exists_linearIndependent_cons_of_lt_finrank
- exists_linearIndependent_pair_of_one_lt_finrank
- LinearMap.lift_rank_comap_le
- exists_linearIndependent_snoc_of_lt_finrank
- Submodule.exists_of_finrank_lt
- LinearMap.lift_rank_eq_of_surjective
- Submodule.exists_smul_notMem_of_rank_lt
Ancestors0
No ancestors.