Rank

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

Statistics

Metric	Count
Definitions cRank, eRank, rank	3
Theorems rank_matrix, cRank_diagonal, cRank_le_card_height, cRank_le_card_width, cRank_one, cRank_reindex, cRank_submatrix, cRank_submatrix_le, cRank_subsingleton, cRank_toNat_eq_finrank, cRank_toNat_eq_rank, cRank_zero, eRank_diagonal, eRank_le_card_height, eRank_le_card_width, eRank_one, eRank_reindex, eRank_submatrix, eRank_submatrix_le, eRank_subsingleton, eRank_toNat_eq_finrank, eRank_toNat_eq_rank, eRank_zero, ker_mulVecLin_conjTranspose_mul_self, ker_mulVecLin_transpose_mul_self, lift_cRank_reindex, lift_cRank_submatrix, lift_cRank_submatrix_le, rank_add_rank_le_card_of_mul_eq_zero, rank_conjTranspose, rank_conjTranspose_mul_self, rank_diagonal, rank_eq_finrank_range_toLin, rank_eq_finrank_span_cols, rank_eq_finrank_span_row, rank_le_card_height, rank_le_card_width, rank_le_height, rank_le_width, rank_mul_eq_left_of_isUnit_det, rank_mul_eq_right_of_isUnit_det, rank_mul_le, rank_mul_le_left, rank_mul_le_right, rank_of_isUnit, rank_one, rank_reindex, rank_self_mul_conjTranspose, rank_self_mul_transpose, rank_submatrix, rank_submatrix_le, rank_subsingleton, rank_transpose, rank_transpose_mul_self, rank_unit, rank_vecMulVec, rank_vecMulVec_le, rank_zero	58
Total	61

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_matrix 📖	mathematical	LinearIndependent Matrix.row DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule	Matrix.rank Fintype.card	—	Matrix.rank_eq_finrank_span_row Finite.of_fintype linearIndependent_iff_card_eq_finrank_span CommRing.orzechProperty IsLocalRing.toNontrivial Field.instIsLocalRing Set.finrank.eq_1

Matrix

Definitions

Name	Category	Theorems
cRank 📖	CompOp	14 math math: lift_cRank_submatrix_le, cRank_subsingleton, lift_cRank_submatrix, cRank_le_card_height, cRank_toNat_eq_rank, cRank_toNat_eq_finrank, cRank_le_card_width, cRank_diagonal, cRank_reindex, cRank_one, lift_cRank_reindex, cRank_submatrix, cRank_zero, cRank_submatrix_le
eRank 📖	CompOp	11 math math: eRank_le_card_width, eRank_le_card_height, eRank_submatrix, eRank_reindex, eRank_one, eRank_toNat_eq_finrank, eRank_diagonal, eRank_zero, eRank_subsingleton, eRank_toNat_eq_rank, eRank_submatrix_le
rank 📖	CompOp	34 math math: rank_transpose, rank_add_rank_le_card_of_mul_eq_zero, LinearIndependent.rank_matrix, IsHermitian.rank_eq_rank_diagonal, rank_one, rank_mul_le_right, rank_of_isUnit, rank_conjTranspose, cRank_toNat_eq_rank, rank_vecMulVec_le, rank_mul_eq_right_of_isUnit_det, rank_eq_finrank_range_toLin, rank_eq_finrank_span_row, rank_transpose_mul_self, rank_submatrix, rank_zero, rank_le_card_width, rank_reindex, rank_self_mul_conjTranspose, rank_subsingleton, rank_diagonal, rank_le_card_height, rank_le_height, rank_mul_le_left, eRank_toNat_eq_rank, rank_mul_eq_left_of_isUnit_det, IsHermitian.rank_eq_card_non_zero_eigs, rank_submatrix_le, rank_mul_le, rank_unit, rank_eq_finrank_span_cols, rank_conjTranspose_mul_self, rank_le_width, rank_self_mul_transpose

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cRank_diagonal 📖	mathematical	—	cRank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Cardinal.lift	—	Pi.linearIndependent_single_of_ne_zero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Pi.single.congr_simp Pi.single_apply LinearIndependent.comp Subtype.val_injective diagonal_transpose Set.instReflSubset Set.instAntisymmSubset cRank.eq_1 Submodule.span_insert_zero rank_span commRing_strongRankCondition Cardinal.lift_umax Cardinal.mk_range_eq_of_injective LinearIndependent.injective Cardinal.lift_id'
cRank_le_card_height 📖	mathematical	—	Cardinal Cardinal.instLE cRank Cardinal.instNatCast Fintype.card	—	LE.le.trans Submodule.rank_le rank_fun' le_refl
cRank_le_card_width 📖	mathematical	—	Cardinal Cardinal.instLE cRank Cardinal.instNatCast Fintype.card	—	LE.le.trans rank_span_le Cardinal.mk_fintype Cardinal.lift_natCast Cardinal.mk_range_le_lift
cRank_one 📖	mathematical	—	cRank CommSemiring.toSemiring CommRing.toCommSemiring Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Cardinal.lift	—	transpose_one one_eq_pi_single Pi.linearIndependent_single_one cRank.eq_1 rank_span commRing_strongRankCondition Cardinal.lift_umax Cardinal.mk_range_eq_of_injective LinearIndependent.injective Cardinal.lift_id'
cRank_reindex 📖	mathematical	—	cRank CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	cRank_submatrix
cRank_submatrix 📖	mathematical	—	cRank CommSemiring.toSemiring CommRing.toCommSemiring submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	lift_cRank_submatrix
cRank_submatrix_le 📖	mathematical	—	Cardinal Cardinal.instLE cRank submatrix	—	lift_cRank_submatrix_le
cRank_subsingleton 📖	mathematical	—	cRank Cardinal Cardinal.instOne	—	rank_subsingleton
cRank_toNat_eq_finrank 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Cardinal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Cardinal.toNat cRank Module.finrank Submodule Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range col Submodule.addCommMonoid Submodule.module	—	—
cRank_toNat_eq_rank 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Cardinal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Cardinal.toNat cRank CommRing.toCommSemiring rank	—	cRank_toNat_eq_finrank rank_eq_finrank_span_cols
cRank_zero 📖	mathematical	—	cRank CommSemiring.toSemiring CommRing.toCommSemiring Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Cardinal Cardinal.instZero	—	isEmpty_or_nonempty cRank.eq_1 Set.range_eq_empty Submodule.span_empty rank_bot transpose_zero Set.range_zero Submodule.span_zero_singleton
eRank_diagonal 📖	mathematical	—	eRank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Set.encard setOf	—	cRank_diagonal Cardinal.toENat_lift
eRank_le_card_height 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat eRank ENat.card	—	ENat.card_eq_coe_fintype_card eRank.eq_1 Cardinal.toENat_le_nat cRank_le_card_height ENat.card_eq_top
eRank_le_card_width 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat eRank ENat.card	—	ENat.card_eq_coe_fintype_card eRank.eq_1 Cardinal.toENat_le_nat cRank_le_card_width ENat.card_eq_top
eRank_one 📖	mathematical	—	eRank CommSemiring.toSemiring CommRing.toCommSemiring Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ENat.card	—	eRank.eq_1 cRank_one Cardinal.toENat_lift ENat.card.eq_1
eRank_reindex 📖	mathematical	—	eRank CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	eRank_submatrix
eRank_submatrix 📖	mathematical	—	eRank CommSemiring.toSemiring CommRing.toCommSemiring submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Cardinal.toENat_lift lift_cRank_submatrix
eRank_submatrix_le 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat eRank submatrix	—	OrderRingHom.instOrderHomClass Cardinal.toENat_lift OrderHom.mono lift_cRank_submatrix_le
eRank_subsingleton 📖	mathematical	—	eRank ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	cRank_subsingleton map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass OrderRingHom.instRingHomClass
eRank_toNat_eq_finrank 📖	mathematical	—	ENat.toNat eRank Module.finrank Submodule Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range col Submodule.addCommMonoid Submodule.module	—	Cardinal.toNat_toENat
eRank_toNat_eq_rank 📖	mathematical	—	ENat.toNat eRank CommSemiring.toSemiring CommRing.toCommSemiring rank	—	eRank_toNat_eq_finrank rank_eq_finrank_span_cols
eRank_zero 📖	mathematical	—	eRank CommSemiring.toSemiring CommRing.toCommSemiring Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ENat instZeroENat	—	cRank_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass OrderRingHom.instRingHomClass
ker_mulVecLin_conjTranspose_mul_self 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id mulVecLin Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	Submodule.ext IsDomain.to_noZeroDivisors instIsDomain
ker_mulVecLin_transpose_mul_self 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id mulVecLin Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain transpose	—	Submodule.ext dotProduct_self_eq_zero vecMul_transpose dotProduct_zero dotProduct_mulVec mulVec_zero
lift_cRank_reindex 📖	mathematical	—	Cardinal.lift cRank CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	lift_cRank_submatrix
lift_cRank_submatrix 📖	mathematical	—	Cardinal.lift cRank CommSemiring.toSemiring CommRing.toCommSemiring submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	LE.le.antisymm lift_cRank_submatrix_le submatrix_submatrix Equiv.self_comp_symm submatrix_id_id
lift_cRank_submatrix_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift cRank submatrix	—	Submodule.rank_mono Submodule.span_mono LE.le.trans Cardinal.lift_monotone RingHomSurjective.ids LinearMap.map_span Set.image_univ Set.image_image transpose_submatrix Set.image_congr cRank.eq_1 lift_rank_map_le
rank_add_rank_le_card_of_mul_eq_zero 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NonUnitalNonAssocSemiring.toAddCommMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	rank Fintype.card	—	Finite.of_fintype RingHomSurjective.ids RingHomInvPair.ids smulCommClass_self rank_eq_finrank_range_toLin Module.finrank_fintype_fun_eq_card commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing LinearMap.finrank_range_add_finrank_ker FiniteDimensional.finiteDimensional_pi' Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self add_le_add_iff_left IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Submodule.finrank_mono FiniteDimensional.finiteDimensional_submodule RingHomCompTriple.ids LinearMap.range_le_ker_iff toLin_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
rank_conjTranspose 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing StarRing.toStarAddMonoid	—	le_antisymm LE.le.trans_eq Eq.trans_le rank_conjTranspose_mul_self rank_mul_le_left conjTranspose_conjTranspose
rank_conjTranspose_mul_self 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd RingHomSurjective.ids ker_mulVecLin_conjTranspose_mul_self LinearMap.finrank_range_add_finrank_ker FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self
rank_diagonal 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fintype.card Subtype.fintype	—	rank.eq_1 RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass toLin'_apply' Module.finrank.eq_1 LinearMap.rank.eq_1 LinearMap.rank_diagonal Cardinal.toNat_natCast
rank_eq_finrank_range_toLin 📖	mathematical	—	rank Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Submodule.addCommMonoid Submodule.module	—	nonempty_fintype RingHomSurjective.ids RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearEquiv.finrank_eq RingHomSurjective.invPair RingHomCompTriple.ids LinearMap.range_comp LinearMap.range_comp_of_range_eq_top LinearEquiv.range LinearMap.pi_ext' LinearMap.ext_ring toLin_self Module.Basis.equiv_apply Pi.basisFun_apply Function.smulCommClass Algebra.to_smulCommClass toLin'_apply' toLin_eq_toLin' map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass
rank_eq_finrank_span_cols 📖	mathematical	—	rank Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range col Submodule.addCommMonoid Submodule.module	—	rank.eq_1 RingHomSurjective.ids range_mulVecLin
rank_eq_finrank_span_row 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain Module.finrank Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.range row Submodule.addCommMonoid Submodule.module	—	nonempty_fintype rank_transpose rank_eq_finrank_span_cols col_transpose
rank_le_card_height 📖	mathematical	—	rank Fintype.card	—	LE.le.trans Submodule.finrank_le commRing_strongRankCondition Module.Finite.pi Finite.of_fintype Module.Finite.self Eq.le Module.finrank_pi
rank_le_card_width 📖	mathematical	—	rank Fintype.card	—	LE.le.trans_eq RingHomSurjective.ids LinearMap.finrank_range_le commRing_strongRankCondition Module.Finite.pi Finite.of_fintype Module.Finite.self Module.finrank_pi
rank_le_height 📖	mathematical	—	rank Fin.fintype	—	LE.le.trans rank_le_card_height Eq.le Fintype.card_fin
rank_le_width 📖	mathematical	—	rank Fin.fintype	—	LE.le.trans rank_le_card_width Eq.le Fintype.card_fin
rank_mul_eq_left_of_isUnit_det 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	rank Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	mulVec_mulVec mul_nonsing_inv one_mulVec rank.eq_1 RingHomCompTriple.ids mulVecLin_mul RingHomSurjective.ids LinearMap.range_comp_of_range_eq_top LinearMap.range_eq_top
rank_mul_eq_right_of_isUnit_det 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	rank Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self LinearEquiv.eq_symm_apply RingHomCompTriple.ids LinearMap.ext mulVecLin_mul mulVec_mulVec LinearMap.comp.congr_simp LinearEquiv.coe_ofIsUnitDet rank.eq_1 RingHomSurjective.ids LinearMap.range_comp LinearEquiv.finrank_map_eq
rank_mul_le 📖	mathematical	—	rank Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	le_min rank_mul_le_left rank_mul_le_right
rank_mul_le_left 📖	mathematical	—	rank Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton rank.eq_1 RingHomCompTriple.ids mulVecLin_mul Cardinal.toNat_le_toNat LinearMap.rank_comp_le_left Module.rank_lt_aleph0 commRing_strongRankCondition Module.Finite.range Module.Finite.pi Finite.of_fintype Module.Finite.self
rank_mul_le_right 📖	mathematical	—	rank Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton rank.eq_1 RingHomCompTriple.ids mulVecLin_mul Module.finrank_le_finrank_of_rank_le_rank LinearMap.lift_rank_comp_le_right Module.rank_lt_aleph0 commRing_strongRankCondition Module.Finite.range Module.Finite.pi Finite.of_fintype Module.Finite.self
rank_of_isUnit 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	rank Fintype.card	—	rank_unit
rank_one 📖	mathematical	—	rank Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Fintype.card	—	rank.eq_1 mulVecLin_one RingHomSurjective.ids LinearMap.range_id finrank_top Module.finrank_pi commRing_strongRankCondition
rank_reindex 📖	mathematical	—	rank DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	rank.eq_1 RingHomCompTriple.ids RingHomInvPair.ids mulVecLin_reindex RingHomSurjective.ids LinearMap.range_comp RingHomSurjective.invPair LinearEquiv.range Submodule.map_top LinearEquiv.finrank_map_eq
rank_self_mul_conjTranspose 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	conjTranspose_conjTranspose rank_conjTranspose rank_conjTranspose_mul_self
rank_self_mul_transpose 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transpose	—	transpose_transpose rank_transpose rank_transpose_mul_self
rank_submatrix 📖	mathematical	—	rank submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	rank_reindex
rank_submatrix_le 📖	mathematical	—	rank submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	rank.eq_1 RingHomCompTriple.ids mulVecLin_submatrix RingHomSurjective.ids LinearMap.range_comp RingHomInvPair.ids RingHomSurjective.invPair LinearEquiv.range Submodule.map_top Submodule.finrank_map_le commRing_strongRankCondition Module.Finite.range Module.Finite.pi Finite.of_fintype Module.Finite.self
rank_subsingleton 📖	mathematical	—	rank	—	Module.finrank_subsingleton
rank_transpose 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain transpose	—	smulCommClass_self RingHomSurjective.ids RingHomInvPair.ids Finite.of_fintype rank_eq_finrank_range_toLin LinearMap.instSMulCommClass toLin_transpose LinearMap.dualMap_def LinearMap.finrank_range_dualMap_eq_finrank_range toLin_eq_toLin' Function.smulCommClass Algebra.to_smulCommClass toLin'_apply' rank.eq_1
rank_transpose_mul_self 📖	mathematical	—	rank EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transpose	—	add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd RingHomSurjective.ids ker_mulVecLin_transpose_mul_self LinearMap.finrank_range_add_finrank_ker FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self
rank_unit 📖	mathematical	—	rank Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring Fintype.card	—	le_antisymm rank_le_card_width rank_mul_le_left rank_one Units.val_one mul_inv_cancel Units.val_mul
rank_vecMulVec 📖	mathematical	—	Cardinal Cardinal.instLE LinearMap.rank CommRing.toRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' vecMulVec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Cardinal.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass rank_subsingleton vecMulVec_eq RingHomCompTriple.ids toLin'_mul le_trans LinearMap.rank_comp_le_left LE.le.trans_eq LinearMap.rank_le_domain rank_fun' commRing_strongRankCondition Fintype.card_ofSubsingleton Nat.cast_one
rank_vecMulVec_le 📖	mathematical	—	rank vecMulVec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	vecMulVec_eq le_trans rank_mul_le_left Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton rank_le_card_width
rank_zero 📖	mathematical	—	rank Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	rank.eq_1 mulVecLin_zero LinearMap.range_zero finrank_bot

---

← Back to Index