InvariantBasisNumber

📁 Source: Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Statistics

Metric	Count
Definitions RankCondition	1
Theorems eq_of_fin_equiv, strongRankCondition, exists_nat_not_surjective, le_of_fin_surjective, le_of_fin_injective, card_eq_of_linearEquiv, card_le_of_injective, card_le_of_injective', card_le_of_surjective, card_le_of_surjective', eq_of_fin_equiv, invariantBasisNumber_iff, invariantBasisNumber_of_nontrivial_of_commRing, invariantBasisNumber_of_rankCondition, le_of_fin_injective, le_of_fin_surjective, nontrivial_of_invariantBasisNumber, rankCondition_iff, rankCondition_of_strongRankCondition, strongRankCondition_iff, strongRankCondition_iff_forall_not_injective, strongRankCondition_iff_succ, strongRankCondition_of_orzechProperty	23
Total	24

InvariantBasisNumber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_fin_equiv 📖	—	—	—	—	—

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strongRankCondition 📖	mathematical	—	StrongRankCondition Ring.toSemiring	—	strongRankCondition_of_orzechProperty orzechProperty

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_not_surjective 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	exists_fin' IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd le_of_fin_surjective RingHomCompTriple.ids

RankCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_fin_surjective 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	—	—

StrongRankCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_fin_injective 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	—	—

(root)

Definitions

Name	Category	Theorems
RankCondition 📖	CompData	8 math math: instRankConditionMulOpposite, rankCondition_iff_le_of_comp_eq_one, rankCondition_iff, instRankConditionOfIsStablyFiniteRingOfNontrivial, rankCondition_of_nontrivial_of_commSemiring, rankCondition_of_strongRankCondition, rankCondition_iff_matrix, MulOpposite.rankCondition_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_of_linearEquiv 📖	mathematical	—	Fintype.card	—	RingHomInvPair.ids eq_of_fin_equiv RingHomCompTriple.ids
card_le_of_injective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	Fintype.card	—	RingHomInvPair.ids le_of_fin_injective RingHomCompTriple.ids LinearEquiv.injective
card_le_of_injective' 📖	mathematical	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike	Fintype.card	—	RingHomInvPair.ids Finite.of_fintype card_le_of_injective RingHomCompTriple.ids LinearEquiv.injective
card_le_of_surjective 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	Fintype.card	—	RingHomInvPair.ids le_of_fin_surjective RingHomCompTriple.ids LinearEquiv.surjective
card_le_of_surjective' 📖	mathematical	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike	Fintype.card	—	RingHomInvPair.ids Finite.of_fintype card_le_of_surjective RingHomCompTriple.ids LinearEquiv.surjective
eq_of_fin_equiv 📖	—	—	—	—	InvariantBasisNumber.eq_of_fin_equiv
invariantBasisNumber_iff 📖	mathematical	—	InvariantBasisNumber	—	RingHomInvPair.ids
invariantBasisNumber_of_nontrivial_of_commRing 📖	mathematical	—	InvariantBasisNumber CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHomInvPair.ids Ideal.exists_maximal eq_of_fin_equiv invariantBasisNumber_of_rankCondition rankCondition_of_strongRankCondition IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Ideal.instIsTwoSided_1 RingHomCompTriple.ids Ideal.instIsTwoSidedForallPi
invariantBasisNumber_of_rankCondition 📖	mathematical	—	InvariantBasisNumber	—	RingHomInvPair.ids le_antisymm le_of_fin_surjective LinearEquiv.surjective
le_of_fin_injective 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	—	StrongRankCondition.le_of_fin_injective
le_of_fin_surjective 📖	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	—	RankCondition.le_of_fin_surjective
nontrivial_of_invariantBasisNumber 📖	mathematical	—	Nontrivial	—	zero_ne_one eq_of_fin_equiv
rankCondition_iff 📖	mathematical	—	RankCondition	—	—
rankCondition_of_strongRankCondition 📖	mathematical	—	RankCondition	—	le_of_fin_injective Finite.of_fintype LinearMap.splittingOfFunOnFintypeSurjective_injective
strongRankCondition_iff 📖	mathematical	—	StrongRankCondition	—	—
strongRankCondition_iff_forall_not_injective 📖	mathematical	—	StrongRankCondition Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.addCommMonoid Finsupp.module Semiring.toModule Pi.Function.module LinearMap.instFunLike	—	strongRankCondition_iff_succ not_iff_not Mathlib.Tactic.Push.not_forall_eq LinearMap.exists_finsupp_nat_of_fin_fun_injective RingHomCompTriple.ids RingHomInvPair.ids Finite.of_fintype Finsupp.mapDomain_injective Fin.val_injective
strongRankCondition_iff_succ 📖	mathematical	—	StrongRankCondition DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike	—	le_of_fin_injective RingHomCompTriple.ids not_le Function.extend_injective StrictMono.injective Fin.strictMono_castLE
strongRankCondition_of_orzechProperty 📖	mathematical	—	StrongRankCondition	—	strongRankCondition_iff_succ OrzechProperty.injective_of_surjective_of_injective Module.Finite.pi Finite.of_fintype Module.Finite.self Function.Injective.surjective_comp_right Nontrivial.to_nonempty Fin.castSucc_injective Function.update_of_ne Function.update_self NeZero.one

---

← Back to Index