LinearMap

📁 Source: Mathlib/Algebra/DirectSum/LinearMap.lean

Statistics

Metric	Count
Definitions	0
Theorems diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, mapsTo_biSup_of_mapsTo, toMatrix_directSum_collectedBasis_eq_blockDiagonal', trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero, trace_eq_sum_trace_restrict, trace_eq_sum_trace_restrict', trace_eq_sum_trace_restrict_of_eq_biSup, trace_eq_zero_of_mapsTo_ne	8
Total	8

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne 📖	mathematical	DirectSum.IsInternal Finset SetLike.instMembership Finset.instSetLike Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Submodule.addSubmonoidClass Set.MapsTo DFunLike.coe Module.End instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Bot.bot Submodule.instBot	Matrix.diag LinearEquiv RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Sigma.instFintype Finset.Subtype.fintype Finite.instSigma Finite.of_fintype Sigma.instDecidableEqSigma DirectSum.IsInternal.collectedBasis Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.addSubmonoidClass RingHomInvPair.ids smulCommClass_self Finite.instSigma Finite.of_fintype toMatrix_apply DirectSum.IsInternal.collectedBasis_coe DirectSum.IsInternal.collectedBasis_repr_of_mem_ne Subtype.mem map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
mapsTo_biSup_of_mapsTo 📖	mathematical	Set.MapsTo DFunLike.coe Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe Submodule Submodule.setLike	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership	—	RingHomSurjective.ids Submodule.map_le_iff_le_comap Submodule.map_iSup iSup₂_mono
toMatrix_directSum_collectedBasis_eq_blockDiagonal' 📖	mathematical	DirectSum.IsInternal Submodule CommSemiring.toSemiring Submodule.setLike Submodule.addSubmonoidClass Finite Set.MapsTo DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike SetLike.coe	LinearEquiv RingHomInvPair.ids Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Sigma.instFintype Finite.instSigma Finite.of_fintype Sigma.instDecidableEqSigma DirectSum.IsInternal.collectedBasis Matrix.blockDiagonal' MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SetLike.instMembership Submodule.addCommMonoid Submodule.module restrict	—	Submodule.addSubmonoidClass Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.instSigma Finite.of_fintype toMatrix_apply eq_or_ne Subtype.mem DirectSum.IsInternal.collectedBasis_coe DirectSum.IsInternal.collectedBasis_repr_of_mem DirectSum.IsInternal.collectedBasis_repr_of_mem_ne
trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero 📖	mathematical	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.End.instMul iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Module.End.maxGenEigenspace Top.top Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule instFunLike trace restrict Module.End.mapsTo_maxGenEigenspace_of_comm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	comp RingHomCompTriple.ids	—	smulCommClass_self Module.End.mapsTo_maxGenEigenspace_of_comm RingHomCompTriple.ids Set.MapsTo.comp Commute.refl restrict_commute Commute.symm IsScalarTower.left Algebra.mul_sub_algebraMap_commutes Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing restrict_comp trace_comp_eq_mul_of_commute_of_isNilpotent isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors MulZeroClass.mul_zero Submodule.addSubmonoidClass DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top Module.End.independent_maxGenEigenspace Module.IsReflexive.to_isTorsionFree Module.instIsReflexiveOfFiniteOfProjective Module.Projective.of_free WellFoundedGT.finite_ne_bot_of_iSupIndep wellFoundedGT trace_eq_sum_trace_restrict' Module.IsNoetherian.finite isNoetherian_submodule' Module.free_of_finite_type_torsion_free' Ideal.instIsTorsionFreeSubtypeMemSubmodule Finset.sum_congr Finset.sum_const_zero
trace_eq_sum_trace_restrict 📖	mathematical	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Module.Free DirectSum.IsInternal Submodule.addSubmonoidClass Set.MapsTo DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike SetLike.coe	addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule trace Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ restrict	—	Submodule.addSubmonoidClass smulCommClass_self RingHomInvPair.ids Finite.of_fintype trace_eq_matrix_trace toMatrix_directSum_collectedBasis_eq_blockDiagonal' Matrix.trace_blockDiagonal' Finset.sum_congr
trace_eq_sum_trace_restrict' 📖	mathematical	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Module.Free DirectSum.IsInternal Submodule.addSubmonoidClass Set.MapsTo DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike SetLike.coe	addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule trace Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Set.Finite.toFinset setOf Bot.bot Submodule.instBot restrict	—	Submodule.addSubmonoidClass smulCommClass_self Finset.sum_coe_sort trace_eq_sum_trace_restrict DirectSum.isInternal_ne_bot_iff Fintype.sum_equiv
trace_eq_sum_trace_restrict_of_eq_biSup 📖	mathematical	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Module.Free iSupIndep Finset Finset.instSetLike Submodule.completeLattice Set.MapsTo DFunLike.coe Module.End instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Finset.instMembership mapsTo_biSup_of_mapsTo	LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule trace restrict Finset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.addSubmonoidClass DirectSum.isInternal_biSup_submodule_of_iSupIndep RingHomInvPair.ids le_biSup Module.Finite.equiv Module.Free.of_equiv smulCommClass_self trace_eq_sum_trace_restrict Finset.sum_coe_sort Finset.sum_congr trace_conj'
trace_eq_zero_of_mapsTo_ne 📖	mathematical	Module.Finite Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Module.Free DirectSum.IsInternal Submodule.addSubmonoidClass Set.MapsTo DFunLike.coe Module.End instFunLike RingHom.id Semiring.toNonAssocSemiring SetLike.coe	LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule trace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Submodule.addSubmonoidClass WellFoundedGT.finite_ne_bot_of_iSupIndep wellFoundedGT DirectSum.IsInternal.submodule_iSupIndep Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable Function.hfunext DirectSum.isInternal_ne_bot_iff smulCommClass_self RingHomInvPair.ids Finite.of_fintype trace_eq_matrix_trace Finset.sum_congr Finite.instSigma diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne Finset.sum_const_zero

---

← Back to Index