Theorems · Inductive type · linear algebra
HasRankNullity
(R : Type v) → [inst : Ring R] → Prop
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.
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement · cited by 7,463
Cited by28
Results whose statement or proof uses this declaration.
- Submodule.finrank_quotient_add_finrankstatement and proof · cited by 13
- Submodule.rank_quotient_add_rankstatement and proof · cited by 8
- exists_set_linearIndependentstatement and proof · cited by 2
- LinearMap.rank_eq_of_surjectivestatement and proof · cited by 2
- Submodule.rank_sup_add_rank_inf_eqstatement and proof · cited by 2
- HasRankNullity.rank_quotient_add_rankstatement and proof · cited by 2
- exists_linearIndependent_cons_of_lt_rankstatement and proof · cited by 2
- exists_linearIndependent_pair_of_one_lt_rankstatement and proof · cited by 2
- exists_linearIndependent_snoc_of_lt_rankstatement and proof · cited by 2
- Submodule.disjoint_ker_of_finrank_lestatement and proof · cited by 2
- LinearMap.lift_rank_range_add_rank_kerstatement and proof · cited by 2
- Submodule.rank_add_le_rank_add_rankstatement and proof · cited by 1