Finite

📁 Source: Mathlib/LinearAlgebra/Dimension/Finite.lean

Statistics

Metric	Count
Definitions fintypeIndexOfRankLtAleph0, fintypeNeBotOfFiniteDimensional	2
Theorems cardinalMk_le_finrank, finite, finrank_eq_zero_of_infinite, finset_card_le_finrank, fintype_card_le_finrank, lt_aleph0_of_finite, setFinite, finite_index_of_rank_lt_aleph0, nonempty_fintype_index_of_rank_lt_aleph0, not_linearIndependent_of_infinite, exists_nontrivial_relation_of_finrank_lt_card, exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card, finite_finsupp_iff, finite_finsupp_self_iff, finite_of_rank_eq_nat, finite_of_rank_eq_one, finite_of_rank_eq_zero, finrank_eq_zero_iff, finrank_eq_zero_of_rank_eq_zero, finrank_pos, finrank_pos_iff, finrank_pos_iff_exists_ne_zero, finrank_quotient_add_finrank_le, finrank_zero_iff, finrank_zero_of_subsingleton, nontrivial_of_finrank_eq_succ, nontrivial_of_finrank_pos, finrank_empty, bot_eq_top_of_rank_eq_zero, finrank_eq_zero, one_le_finrank_iff, rank_eq_zero, exists_finset_linearIndependent_of_le_finrank, exists_finset_linearIndependent_of_le_rank, exists_linearIndependent_of_le_finrank, exists_linearIndependent_of_le_rank, exists_mem_ne_zero_of_rank_pos, exists_set_linearIndependent_of_lt_rank, finrank_bot, finrank_eq_one, finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_not_finite, finrank_eq_zero_of_not_exists_basis, finrank_eq_zero_of_not_exists_basis_finite, finrank_eq_zero_of_not_exists_basis_finset, finrank_le_one, subtype_ne_bot_le_finrank, subtype_ne_bot_le_finrank_aux, subtype_ne_bot_le_rank, linearIndependent_bounded_of_finset_linearIndependent_bounded, natCast_le_rank_iff, natCast_le_rank_iff_finset, rank_eq_one, rank_eq_zero_iff, rank_le, rank_le_one, rank_pos, rank_pos_iff_exists_ne_zero, rank_pos_iff_nontrivial, rank_zero_iff, rank_zero_iff_forall_zero	61
Total	63

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_le_finrank 📖	mathematical	LinearIndependent	Cardinal Cardinal.instLE Cardinal.instNatCast Module.finrank	—	Cardinal.lift_le Cardinal.lift_natCast cardinal_lift_le_rank nontrivial_of_invariantBasisNumber invariantBasisNumber_of_rankCondition rankCondition_of_strongRankCondition
finite 📖	mathematical	LinearIndependent	Finite	—	Cardinal.lt_aleph0_iff_finite lt_aleph0_of_finite
finrank_eq_zero_of_infinite 📖	mathematical	LinearIndependent	Module.finrank	—	Cardinal.toNat_eq_zero aleph0_le_rank
finset_card_le_finrank 📖	mathematical	LinearIndependent Finset SetLike.instMembership Finset.instSetLike	Finset.card Module.finrank	—	Fintype.card_coe fintype_card_le_finrank
fintype_card_le_finrank 📖	mathematical	LinearIndependent	Fintype.card Module.finrank	—	Cardinal.mk_fintype Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero cardinalMk_le_finrank
lt_aleph0_of_finite 📖	mathematical	LinearIndependent	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.aleph0	—	Cardinal.lift_lt lt_of_le_of_lt cardinal_lift_le_rank nontrivial_of_invariantBasisNumber invariantBasisNumber_of_rankCondition rankCondition_of_strongRankCondition Module.finrank_eq_rank Cardinal.lift_aleph0 Cardinal.lift_natCast Cardinal.natCast_lt_aleph0
setFinite 📖	mathematical	LinearIndependent Set.Elem Set Set.instMembership	Set.Finite	—	Cardinal.lt_aleph0_iff_set_finite lt_aleph0_of_finite

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nontrivial_relation_of_finrank_lt_card 📖	mathematical	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid Finset.card	Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finset Finset.instMembership	—	Fintype.not_linearIndependent_iff LinearIndependent.finset_card_le_finrank LT.lt.not_ge Finset.sum_finset_coe Finset.sum_congr Function.Injective.extend_apply Subtype.val_injective
exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card 📖	mathematical	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid Finset.card	Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finset Finset.instMembership	—	Finset.card_pos LT.lt.trans sub_left_injective Finset.card_map Finset.card_erase_of_mem exists_nontrivial_relation_of_finrank_lt_card Finset.sum_congr Finset.sum_erase_add neg_smul Finset.sum_smul Finset.sum_map smul_sub Finset.mem_erase Finset.mem_map
finite_finsupp_iff 📖	mathematical	—	Finite Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module IsEmpty Finite	—	Finite.of_surjective RingHomSurjective.ids Finsupp.apply_surjective finite_of_span_finite_eq_top_finsupp Finset.finite_toSet IsNoetherian.finite isNoetherian_of_finite Finite.of_fintype Finite.finsupp
finite_finsupp_self_iff 📖	mathematical	—	Finite Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Finite	—	Finite.of_subsingleton IsEmpty.instSubsingleton
finite_of_rank_eq_nat 📖	mathematical	rank Cardinal Cardinal.instNatCast	Finite	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim IsNoetherian.finite isNoetherian_of_subsingleton Free.exists_basis Cardinal.mk_lt_aleph0_iff LE.le.trans_lt LE.le.trans_eq LinearIndependent.cardinal_le_rank Basis.linearIndependent Cardinal.natCast_lt_aleph0 Finite.of_basis
finite_of_rank_eq_one 📖	mathematical	rank Cardinal Cardinal.instOne	Finite	—	finite_of_rank_eq_nat Nat.cast_one
finite_of_rank_eq_zero 📖	mathematical	rank Ring.toSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero	Finite	—	IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton rank_zero_iff
finrank_eq_zero_iff 📖	mathematical	—	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	rank_eq_zero_iff finrank_eq_rank Nat.cast_zero Cardinal.instCharZero
finrank_eq_zero_of_rank_eq_zero 📖	mathematical	rank Cardinal Cardinal.instZero	finrank	—	Cardinal.zero_toNat
finrank_pos 📖	mathematical	—	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid	—	finrank_pos_iff
finrank_pos_iff 📖	mathematical	—	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid Nontrivial	—	rank_pos_iff_nontrivial finrank_eq_rank Nat.cast_zero Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero
finrank_pos_iff_exists_ne_zero 📖	mathematical	—	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid	—	rank_pos_iff_exists_ne_zero finrank_eq_rank Nat.cast_zero Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero
finrank_quotient_add_finrank_le 📖	mathematical	—	finrank HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	rank_quotient_add_rank_le nontrivial_of_invariantBasisNumber invariantBasisNumber_of_rankCondition rankCondition_of_strongRankCondition Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero Submodule.finrank_eq_rank finrank_eq_rank Finite.quotient
finrank_zero_iff 📖	mathematical	—	finrank Ring.toSemiring AddCommGroup.toAddCommMonoid	—	rank_zero_iff finrank_eq_rank Nat.cast_zero Cardinal.instCharZero
finrank_zero_of_subsingleton 📖	mathematical	—	finrank	—	finrank.eq_1 rank_subsingleton' map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
nontrivial_of_finrank_eq_succ 📖	mathematical	finrank	Nontrivial	—	nontrivial_of_finrank_pos
nontrivial_of_finrank_pos 📖	mathematical	finrank	Nontrivial	—	Mathlib.Tactic.Contrapose.contrapose₁ Eq.le finrank_zero_of_subsingleton

Module.Basis

Definitions

Name	Category	Theorems
fintypeIndexOfRankLtAleph0 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_index_of_rank_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Module.rank Cardinal.aleph0	Set.Finite	—	Set.finite_def nonempty_fintype_index_of_rank_lt_aleph0
nonempty_fintype_index_of_rank_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Module.rank Cardinal.aleph0	Fintype	—	Cardinal.lt_aleph0_iff_fintype Cardinal.lift_lt_aleph0 Cardinal.lift_aleph0 mk_eq_rank Cardinal.lift_lt

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_linearIndependent_of_infinite 📖	mathematical	—	LinearIndependent	—	LinearIndependent.finite not_finite

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_empty 📖	mathematical	—	finrank Set instEmptyCollection	—	finrank.eq_1 Submodule.span_empty finrank_bot

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_top_of_rank_eq_zero 📖	mathematical	Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero	Bot.bot Submodule instBot Top.top instTop	—	Unique.instSubsingleton rank_zero_iff
finrank_eq_zero 📖	mathematical	—	Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module Bot.bot instBot	—	rank_eq_zero Module.finrank_eq_rank Nat.cast_zero Cardinal.instCharZero
one_le_finrank_iff 📖	mathematical	—	Module.finrank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module	—	Mathlib.Tactic.Contrapose.contrapose_iff₃ finrank_eq_zero
rank_eq_zero 📖	mathematical	—	Module.rank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module Cardinal Cardinal.instZero Bot.bot instBot	—	eq_bot_iff bot_eq_top_of_rank_eq_zero Ideal.instIsTorsionFreeSubtypeMemSubmodule mem_top rank_bot IsDomain.toNontrivial

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finset_linearIndependent_of_le_finrank 📖	mathematical	Module.finrank	Finset.card LinearIndependent Finset SetLike.instMembership Finset.instSetLike	—	le_zero_iff LE.le.trans_eq linearIndependent_empty exists_finset_linearIndependent_of_le_rank Nat.cast_le Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero Cardinal.cast_toNat_of_lt_aleph0 Cardinal.toNat_ne_zero
exists_finset_linearIndependent_of_le_rank 📖	mathematical	Cardinal Cardinal.instLE Cardinal.instNatCast Module.rank	Finset.card LinearIndepOn SetLike.coe Finset Finset.instSetLike	—	LE.le.eq_or_lt Cardinal.exists_eq_natCast_of_iSup_eq nonempty_linearIndependent_set Cardinal.bddAbove_range small_subtype small_set UnivLE.small UnivLE.self Module.rank_def Cardinal.lt_aleph0_iff_finite Cardinal.natCast_lt_aleph0 nonempty_fintype Set.toFinset_card Cardinal.mk_fintype Cardinal.instCharZero Set.coe_toFinset exists_set_linearIndependent_of_lt_rank
exists_linearIndependent_of_le_finrank 📖	mathematical	Module.finrank	LinearIndependent	—	exists_finset_linearIndependent_of_le_finrank linearIndependent_equiv
exists_linearIndependent_of_le_rank 📖	mathematical	Cardinal Cardinal.instLE Cardinal.instNatCast Module.rank	LinearIndependent	—	exists_finset_linearIndependent_of_le_rank linearIndependent_equiv
exists_mem_ne_zero_of_rank_pos 📖	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero Module.rank Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	—	Submodule.exists_mem_ne_zero_of_ne_bot lt_irrefl rank_bot
exists_set_linearIndependent_of_lt_rank 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Module.rank	Set.Elem LinearIndepOn	—	exists_lt_of_lt_ciSup' LT.lt.trans_eq Module.rank_def Cardinal.le_mk_iff_exists_subset LT.lt.le LinearIndepOn.mono
finrank_bot 📖	mathematical	—	Module.finrank Submodule SetLike.instMembership Submodule.setLike Bot.bot Submodule.instBot Submodule.addCommMonoid Submodule.module	—	Module.finrank_eq_of_rank_eq rank_bot
finrank_eq_one 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Module.finrank	—	Module.finrank_eq_of_rank_eq rank_eq_one
finrank_eq_zero_of_basis_imp_false 📖	mathematical	—	Module.finrank	—	finrank_eq_zero_of_basis_imp_not_finite Set.Finite.coe_toFinset
finrank_eq_zero_of_basis_imp_not_finite 📖	mathematical	Set.Finite	Module.finrank	—	subsingleton_or_nontrivial Module.subsingleton Unique.instSubsingleton Set.instIsEmptyElemEmptyCollection Set.finite_empty Module.free_iff_set Set.Infinite.to_subtype LinearIndependent.finrank_eq_zero_of_infinite Module.Basis.linearIndependent
finrank_eq_zero_of_not_exists_basis 📖	mathematical	Module.Basis Set.Elem SetLike.coe Finset Finset.instSetLike	Module.finrank	—	finrank_eq_zero_of_basis_imp_false
finrank_eq_zero_of_not_exists_basis_finite 📖	mathematical	Set.Finite	Module.finrank	—	finrank_eq_zero_of_basis_imp_not_finite
finrank_eq_zero_of_not_exists_basis_finset 📖	mathematical	Module.Basis Finset SetLike.instMembership Finset.instSetLike	Module.finrank	—	finrank_eq_zero_of_basis_imp_false
finrank_le_one 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Module.finrank	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Module.finrank.eq_1 Cardinal.toNat_le_toNat rank_le_one Cardinal.one_lt_aleph0
linearIndependent_bounded_of_finset_linearIndependent_bounded 📖	mathematical	Finset.card LinearIndependent Set Set.instMembership	Cardinal Cardinal.instLE Set.Elem Cardinal.instNatCast	—	Cardinal.card_le_of Finset.card_map linearIndependent_finset_map_embedding_subtype
natCast_le_rank_iff 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.instNatCast Module.rank LinearIndependent	—	exists_linearIndependent_of_le_rank Cardinal.mk_fintype Fintype.card_fin Cardinal.lift_natCast Cardinal.lift_uzero LinearIndependent.cardinal_lift_le_rank
natCast_le_rank_iff_finset 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.instNatCast Module.rank Finset.card LinearIndependent Finset SetLike.instMembership Finset.instSetLike	—	exists_finset_linearIndependent_of_le_rank Cardinal.mk_fintype Fintype.card_coe LinearIndependent.cardinal_le_rank
rank_eq_one 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Module.rank Cardinal Cardinal.instOne	—	Module.Basis.basis_singleton_iff rank_eq_card_basis Fintype.card_punit Nat.cast_one
rank_eq_zero_iff 📖	mathematical	—	Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton NeZero.charZero_one Cardinal.instCharZero Unique.instSubsingleton Zero.instNonempty Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq Cardinal.one_le_iff_ne_zero linearIndependent_iff Finsupp.unique_ext Finsupp.linearCombination_unique Cardinal.mk_fintype Fintype.card_unique Nat.cast_one Cardinal.lift_one Cardinal.lift_uzero LinearIndependent.cardinal_lift_le_rank nonpos_iff_eq_zero Cardinal.canonicallyOrderedAdd Module.rank_def ciSup_le' Cardinal.mk_eq_zero_iff not_nonempty_iff Finsupp.single_eq_same DFunLike.congr_fun Finsupp.linearCombination_single
rank_le 📖	mathematical	Finset.card	Cardinal Cardinal.instLE Module.rank Cardinal.instNatCast	—	Module.rank_def ciSup_le' linearIndependent_bounded_of_finset_linearIndependent_bounded
rank_le_one 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Cardinal Cardinal.instLE Module.rank Cardinal.instOne	—	Module.rank_self Cardinal.lift_one LinearMap.lift_rank_le_of_surjective
rank_pos 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid	—	rank_pos_iff_nontrivial
rank_pos_iff_exists_ne_zero 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ nonpos_iff_eq_zero Cardinal.canonicallyOrderedAdd rank_zero_iff_forall_zero
rank_pos_iff_nontrivial 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid Nontrivial	—	rank_pos_iff_exists_ne_zero nontrivial_iff_exists_ne
rank_zero_iff 📖	mathematical	—	Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero	—	rank_zero_iff_forall_zero
rank_zero_iff_forall_zero 📖	mathematical	—	Module.rank Ring.toSemiring AddCommGroup.toAddCommMonoid Cardinal Cardinal.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsDomain.toIsCancelMulZero exists_ne IsDomain.toNontrivial

iSupIndep

Definitions

Name	Category	Theorems
fintypeNeBotOfFiniteDimensional 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subtype_ne_bot_le_finrank 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	Fintype.card Bot.bot Submodule.instBot Module.finrank	—	Cardinal.mk_fintype Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero subtype_ne_bot_le_finrank_aux
subtype_ne_bot_le_finrank_aux 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	Cardinal Cardinal.instLE Bot.bot Submodule.instBot Cardinal.instNatCast Module.finrank	—	subtype_ne_bot_le_rank Module.finrank_eq_rank Cardinal.lift_natCast Cardinal.lift_le
subtype_ne_bot_le_rank 📖	mathematical	iSupIndep Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.completeLattice	Cardinal Cardinal.instLE Cardinal.lift Bot.bot Submodule.instBot Module.rank	—	Submodule.ne_bot_iff Subtype.prop linearIndependent comp Subtype.coe_injective LinearIndependent.cardinal_lift_le_rank IsDomain.toNontrivial

---

← Back to Index