Theorems · Inductive type · ring theory
InvariantBasisNumber
(R : Type u) → [Semiring R] → Prop
We say that R has the invariant basis number property if (Fin n → R) ≃ₗ[R] (Fin m → R)
implies n = m. This gives rise to a well-defined notion of rank of a finitely generated free
module.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Semiring
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.
- Semiringstatement · cited by 13,802
Cited by16
Results whose statement or proof uses this declaration.
- nontrivial_of_invariantBasisNumberstatement and proof · cited by 18
- Module.Basis.indexEquivstatement and proof · cited by 9
- card_eq_of_linearEquivstatement and proof · cited by 4
- LinearMap.charpoly_natDegreeproof · cited by 3
- eq_of_fin_equivstatement and proof · cited by 2
- Matrix.square_of_invertiblestatement and proof · cited by 1
- InvariantBasisNumber.casesOnstatement and proof · cited by 1
- InvariantBasisNumber.eq_of_fin_equivstatement and proof · cited by 1
- mk_eq_mk_of_basisstatement and proof · cited by 1
- invariantBasisNumber_iffstatement and proof · cited by 1
- invariantBasisNumber_iff_matrixstatement · cited by 0
- CategoryTheory.HomOrthogonal.equiv_of_isostatement and proof · cited by 0