InvariantBasisNumber

📁 Source: Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean

Statistics

Metric	Count
Definitions InvariantBasisNumber	1
Theorems square_of_invertible, invariantBasisNumber_iff, rankCondition_iff, instInvariantBasisNumberMulOpposite, instIsStablyFiniteRingOfOrzechProperty, instRankConditionMulOpposite, instRankConditionOfIsStablyFiniteRingOfNontrivial, invariantBasisNumber_iff_matrix, rankCondition_iff_le_of_comp_eq_one, rankCondition_iff_matrix, rankCondition_of_nontrivial_of_commSemiring	11
Total	12

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
square_of_invertible 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Fintype.card	—	card_eq_of_linearEquiv

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invariantBasisNumber_iff 📖	mathematical	—	InvariantBasisNumber MulOpposite instSemiring	—	Equiv.forall_congr_right Equiv.injective forall_swap AddEquiv.injective Matrix.ext Finset.sum_congr Finset.unop_sum Matrix.map_one Matrix.transpose_one
rankCondition_iff 📖	mathematical	—	RankCondition MulOpposite instSemiring	—	Equiv.forall_congr_right Equiv.injective forall_swap AddEquiv.injective Matrix.ext Finset.sum_congr Finset.unop_sum Matrix.map_one Matrix.transpose_one

(root)

Definitions

Name	Category	Theorems
InvariantBasisNumber 📖	CompData	6 math math: invariantBasisNumber_of_rankCondition, invariantBasisNumber_of_nontrivial_of_commRing, invariantBasisNumber_iff_matrix, MulOpposite.invariantBasisNumber_iff, instInvariantBasisNumberMulOpposite, invariantBasisNumber_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instInvariantBasisNumberMulOpposite 📖	mathematical	—	InvariantBasisNumber MulOpposite MulOpposite.instSemiring	—	MulOpposite.invariantBasisNumber_iff
instIsStablyFiniteRingOfOrzechProperty 📖	mathematical	—	IsStablyFiniteRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	isStablyFiniteRing_iff_injective_of_surjective OrzechProperty.injective_of_surjective_endomorphism Module.Finite.pi Finite.of_fintype Module.Finite.self
instRankConditionMulOpposite 📖	mathematical	—	RankCondition MulOpposite MulOpposite.instSemiring	—	MulOpposite.rankCondition_iff
instRankConditionOfIsStablyFiniteRingOfNontrivial 📖	mathematical	—	RankCondition	—	LT.lt.le LinearMap.funLeft_surjective_of_injective Fin.castLE_injective Function.Injective.of_comp_right Module.End.injective_of_surjective_fin RingHomCompTriple.ids Function.injective_comp_right_iff_surjective LT.lt.ne
invariantBasisNumber_iff_matrix 📖	mathematical	—	InvariantBasisNumber	—	RingHomInvPair.ids invariantBasisNumber_iff Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left RingHomCompTriple.ids LinearEquiv.self_trans_symm LinearMap.toMatrixRight'_id LinearEquiv.symm_trans_self
rankCondition_iff_le_of_comp_eq_one 📖	mathematical	—	RankCondition	—	RingHomCompTriple.ids rankCondition_iff LinearMap.surjective_of_comp_eq_id RingHomInvPair.ids Module.projective_lifting_property Module.Projective.of_free Module.Free.function Finite.of_fintype Module.Free.self
rankCondition_iff_matrix 📖	mathematical	—	RankCondition	—	RingHomCompTriple.ids Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left RingHomInvPair.ids Equiv.forall_congr_right LinearEquiv.injective
rankCondition_of_nontrivial_of_commSemiring 📖	mathematical	—	RankCondition CommSemiring.toSemiring	—	instRankConditionOfIsStablyFiniteRingOfNontrivial Matrix.instIsStablyFiniteRingOfCommSemiring

---

← Back to Index