Theorems · Theorem · linear algebra
Module.finrank_fintype_fun_eq_card
∀ (R : Type u) {η : Type u₁'} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Fintype η],
Module.finrank R (η → R) = Fintype.card ηThe vector space of functions on a Fintype ι has finrank equal to the cardinality of ι.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Fintypestatement and proof · cited by 7,736
- Module.finrankstatement · cited by 1,770
- Fintype.cardstatement · cited by 1,386
- StrongRankConditionstatement and proof · cited by 286
- Module.finrank_eq_of_rank_eqproof · cited by 13
- rank_fun'proof · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- finrank_euclideanSpaceproof · cited by 7
- Module.finrank_fin_funproof · cited by 5
- MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaarproof · cited by 3
- integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrableproof · cited by 2
- MeasureTheory.volume_sum_rpow_lt_oneproof · cited by 2
- QuadraticForm.sigPos_weightedSumSquaresproof · cited by 2
- Projectivization.card_of_finrankproof · cited by 1
- MeasureTheory.lintegral_pow_le_pow_lintegral_fderivproof · cited by 1
- Matrix.rank_add_rank_le_card_of_mul_eq_zeroproof · cited by 1
- NumberField.Units.finrank_eq_rankproof · cited by 1
- AddChar.card_addChar_leproof · cited by 1
- MvPolynomial.ker_evalₗproof · cited by 1