Diagonal

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

Statistics

Metric	Count
Definitions	0
Theorems rank_diagonal, diagonal_comp_single, diagonal_toLin', ker_diagonal_toLin', proj_diagonal, range_diagonal	6
Total	6

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_diagonal 📖	mathematical	—	rank DivisionRing.toRing Field.toDivisionRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid Matrix.addCommMonoid addCommMonoid Matrix.module 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 Matrix.toLin' Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Cardinal Cardinal.instNatCast Fintype.card Subtype.fintype	—	Set.compl_union_self subset_refl Set.instReflSubset disjoint_compl_left RingHomSurjective.ids iSup_range_single_eq_iInf_ker_proj Set.toFinite Subtype.finite Finite.of_fintype RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass rank.eq_1 Matrix.range_diagonal rank_fun' IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain LinearEquiv.rank_eq

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonal_comp_single 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.addCommMonoid Semiring.toModule Pi.Function.module RingHom.id RingHomCompTriple.ids DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap 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' diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass LinearMap.single Pi.module LinearMap.instSMul Pi.distribSMul AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass diagonal_mulVec_single Pi.single_smul'
diagonal_toLin' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule 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' diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass LinearMap.pi Pi.module LinearMap.instSMul instDistribSMul LinearMap.proj	—	LinearMap.ext RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass mulVec_diagonal
ker_diagonal_toLin' 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring Semifield.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap 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' diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring iSup Submodule Pi.module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership setOf LinearMap.range RingHomSurjective.ids LinearMap.single	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass RingHomSurjective.ids Submodule.comap_bot LinearMap.iInf_ker_proj Submodule.comap_iInf RingHomCompTriple.ids LinearMap.ker_comp proj_diagonal LinearMap.ker_smul' Set.union_compl_self subset_refl Set.instReflSubset LinearMap.iSup_range_single_eq_iInf_ker_proj disjoint_compl_right Set.toFinite Subtype.finite Finite.of_fintype
proj_diagonal 📖	mathematical	—	LinearMap.comp CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule Pi.module RingHom.id RingHomCompTriple.ids LinearMap.proj DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap 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' diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass LinearMap.instSMul instDistribSMul	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass mulVec_diagonal
range_diagonal 📖	mathematical	—	LinearMap.range CommSemiring.toSemiring Semifield.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap 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' diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring iSup Submodule Pi.module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership setOf LinearMap.single	—	RingHomSurjective.ids RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Submodule.map_top LinearMap.iSup_range_single Finite.of_fintype Submodule.map_iSup RingHomCompTriple.ids LinearMap.range_comp diagonal_comp_single smulCommClass_self LinearMap.range_smul'

---

← Back to Index