Card

📁 Source: Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean

Statistics

Metric	Count
Definitions equiv_GL_linearindependent	1
Theorems card_GL_field, card_linearIndependent	2
Total	3

Matrix

Definitions

Name	Category	Theorems
equiv_GL_linearindependent 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_GL_field 📖	mathematical	—	Nat.card GeneralLinearGroup Fin.fintype DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Finset.prod Nat.instCommMonoid Finset.univ Monoid.toNatPow Nat.instMonoid Fintype.card	—	Nat.card_congr card_linearIndependent Pi.finite Finite.of_fintype Module.finrank_fintype_fun_eq_card commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Fintype.card_fin

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_linearIndependent 📖	mathematical	Module.finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	Nat.card LinearIndependent Finset.prod Nat.instCommMonoid Finset.univ Fin.fintype Monoid.toNatPow Nat.instMonoid Fintype.card	—	Subtype.finite Pi.finite Finite.of_fintype Nat.card_eq_fintype_card Fintype.card_congr' Unique.instSubsingleton Fin.isEmpty' Finsupp.linearCombination_fin_zero LinearMap.ker_zero Finset.prod_congr Finset.univ_eq_empty Fintype.card_compl_set Submodule.addSubgroupClass Submodule.smulMemClass Module.card_eq_pow_finrank finrank_span_eq_card IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Fintype.card_fin Fintype.card_congr Fintype.card_sigma Fintype.sum_congr Finset.sum_const mul_comm Fin.prod_univ_succAbove Fin.succAbove_last

---

← Back to Index