LapMatrix

📁 Source: Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Statistics

Metric	Count
Definitions degMatrix, lapMatrix, lapMatrix_ker_basis, lapMatrix_ker_basis_aux	4
Theorems card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, degMatrix_mulVec_apply, degree_eq_sum_if_adj, det_lapMatrix_eq_zero, dotProduct_mulVec_degMatrix, isSymm_degMatrix, isSymm_lapMatrix, lapMatrix_mulVec_apply, lapMatrix_mulVec_const_eq_zero, lapMatrix_mulVec_eq_zero_iff_forall_adj, lapMatrix_mulVec_eq_zero_iff_forall_reachable, lapMatrix_toLinearMap₂', lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, linearIndependent_lapMatrix_ker_basis_aux, mem_ker_toLin'_lapMatrix_of_connectedComponent, posSemidef_lapMatrix, top_le_span_range_lapMatrix_ker_basis_aux	18
Total	22

SimpleGraph

Definitions

Name	Category	Theorems
degMatrix 📖	CompOp	3 math math: dotProduct_mulVec_degMatrix, isSymm_degMatrix, degMatrix_mulVec_apply
lapMatrix 📖	CompOp	14 math math: lapMatrix_toLinearMap₂', det_lapMatrix_eq_zero, card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, posSemidef_lapMatrix, lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, lapMatrix_mulVec_const_eq_zero, linearIndependent_lapMatrix_ker_basis_aux, top_le_span_range_lapMatrix_ker_basis_aux, lapMatrix_mulVec_apply, isSymm_lapMatrix, lapMatrix_mulVec_eq_zero_iff_forall_reachable, lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, mem_ker_toLin'_lapMatrix_of_connectedComponent, lapMatrix_mulVec_eq_zero_iff_forall_adj
lapMatrix_ker_basis 📖	CompOp	—
lapMatrix_ker_basis_aux 📖	CompOp	2 math math: linearIndependent_lapMatrix_ker_basis_aux, top_le_span_range_lapMatrix_ker_basis_aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix 📖	mathematical	—	Fintype.card ConnectedComponent instFintypeConnectedComponent Module.finrank Real Submodule CommSemiring.toSemiring Real.instCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.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 Matrix.toLin' lapMatrix Ring.toAddGroupWithOne Real.instRing Real.semiring Submodule.addCommMonoid Submodule.module	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Module.finrank_eq_card_basis commRing_strongRankCondition Real.instNontrivial
degMatrix_mulVec_apply 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring degMatrix AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast degree neighborSetFintype	—	degMatrix.eq_1 Matrix.mulVec_diagonal
degree_eq_sum_if_adj 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne degree neighborSetFintype Finset.sum AddCommMonoidWithOne.toAddCommMonoid Finset.univ Adj AddMonoidWithOne.toOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid	—	Finset.sum_boole Set.toFinset_setOf
det_lapMatrix_eq_zero 📖	mathematical	—	Matrix.det Real Real.commRing lapMatrix Ring.toAddGroupWithOne Real.instRing Real.instZero	—	Matrix.exists_mulVec_eq_zero_iff Real.instIsDomain Function.support_nonempty_iff NeZero.charZero_one RCLike.charZero_rclike lapMatrix_mulVec_eq_zero_iff_forall_adj
dotProduct_mulVec_degMatrix 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.mulVec degMatrix AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.sum Finset.univ AddMonoidWithOne.toNatCast degree neighborSetFintype	—	Finset.sum_congr Matrix.mulVec_diagonal mul_comm
isSymm_degMatrix 📖	mathematical	—	Matrix.IsSymm degMatrix	—	Matrix.isSymm_diagonal
isSymm_lapMatrix 📖	mathematical	—	Matrix.IsSymm lapMatrix	—	Matrix.IsSymm.sub isSymm_degMatrix isSymm_adjMatrix
lapMatrix_mulVec_apply 📖	mathematical	—	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing lapMatrix AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne degree neighborSetFintype Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid neighborFinset	—	Matrix.sub_mulVec degMatrix_mulVec_apply adjMatrix_mulVec_apply
lapMatrix_mulVec_const_eq_zero 📖	mathematical	—	Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing lapMatrix AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	lapMatrix_mulVec_apply mul_one Finset.sum_const nsmul_eq_mul sub_self
lapMatrix_mulVec_eq_zero_iff_forall_adj 📖	mathematical	—	Matrix.mulVec Real NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing lapMatrix Ring.toAddGroupWithOne Real.instRing Pi.instZero Real.instZero	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass Matrix.PosSemidef.toLinearMap₂'_zero_iff posSemidef_lapMatrix Real.instIsStrictOrderedRing instTrivialStarReal TrivialStar.star_trivial Pi.instTrivialStarForall lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj
lapMatrix_mulVec_eq_zero_iff_forall_reachable 📖	mathematical	—	Matrix.mulVec Real NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing lapMatrix Ring.toAddGroupWithOne Real.instRing Pi.instZero Real.instZero	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass Matrix.PosSemidef.toLinearMap₂'_zero_iff posSemidef_lapMatrix Real.instIsStrictOrderedRing instTrivialStarReal TrivialStar.star_trivial Pi.instTrivialStarForall lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable
lapMatrix_toLinearMap₂' 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂' lapMatrix Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Finset.sum Finset.univ Adj Monoid.toNatPow SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass Nat.instAtLeastTwoHAddOfNat Matrix.toLinearMap₂'_apply' Matrix.sub_mulVec dotProduct_sub dotProduct_mulVec_degMatrix dotProduct_mulVec_adjMatrix Finset.sum_congr degree_eq_sum_if_adj Finset.sum_mul ite_mul one_mul MulZeroClass.zero_mul ite_sub_ite sub_zero add_self_div_two CharZero.NeZero.two if_congr adj_comm Finset.sum_comm ite_add_ite Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.pow_zero
lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂' lapMatrix Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass Nat.instAtLeastTwoHAddOfNat lapMatrix_toLinearMap₂' IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Finset.sum_nonneg Mathlib.Meta.Positivity.ite_nonneg Even.pow_nonneg AddGroup.existsAddOfLE even_two_mul Mathlib.Meta.Positivity.nonneg_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors ne_of_gt Mathlib.Meta.Positivity.pos_of_isNat StarOrderedRing.toIsOrderedRing Nat.instStarOrderedRing Nat.instNontrivial
lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable 📖	mathematical	—	DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Real.instAddCommMonoid Pi.Function.module Semiring.toModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid Matrix.module LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLinearMap₂' lapMatrix Ring.toAddGroupWithOne Real.instRing Real.instZero	—	Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj Real.instIsStrictOrderedRing Adj.reachable
linearIndependent_lapMatrix_ker_basis_aux 📖	mathematical	—	LinearIndependent ConnectedComponent Real Submodule CommSemiring.toSemiring Real.instCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.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 Matrix.toLin' lapMatrix Ring.toAddGroupWithOne Real.instRing lapMatrix_ker_basis_aux Real.semiring Submodule.addCommMonoid Submodule.module	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Fintype.linearIndependent_iff Pi.isScalarTower IsScalarTower.right SMulMemClass.smul_mem Submodule.smulMemClass mem_ker_toLin'_lapMatrix_of_connectedComponent Finset.sum_congr AddSubmonoid.coe_finset_sum Finset.sum_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq
mem_ker_toLin'_lapMatrix_of_connectedComponent 📖	mathematical	—	Submodule Real CommSemiring.toSemiring Real.instCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.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 Matrix.toLin' lapMatrix Ring.toAddGroupWithOne Real.instRing ConnectedComponent connectedComponentMk Real.instOne Real.instZero	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass LinearMap.mem_ker Matrix.toLin'_apply lapMatrix_mulVec_eq_zero_iff_forall_reachable ConnectedComponent.eq
posSemidef_lapMatrix 📖	mathematical	—	Matrix.PosSemidef DivisionRing.toRing Field.toDivisionRing SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder lapMatrix Ring.toAddGroupWithOne	—	Matrix.PosSemidef.of_dotProduct_mulVec_nonneg Matrix.IsHermitian.eq_1 Matrix.conjTranspose_eq_transpose_of_trivial isSymm_lapMatrix TrivialStar.star_trivial Pi.instTrivialStarForall Algebra.to_smulCommClass RingHomInvPair.ids LinearMap.instSMulCommClass Matrix.toLinearMap₂'_apply' Nat.instAtLeastTwoHAddOfNat lapMatrix_toLinearMap₂' IsStrictOrderedRing.toCharZero Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Mathlib.Meta.Positivity.ite_nonneg Even.pow_nonneg AddGroup.existsAddOfLE even_two_mul Mathlib.Meta.Positivity.nonneg_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.Positivity.pos_of_isNat IsLocalRing.toNontrivial Field.instIsLocalRing Mathlib.Meta.NormNum.instAtLeastTwo
top_le_span_range_lapMatrix_ker_basis_aux 📖	mathematical	—	Submodule Real CommSemiring.toSemiring Real.instCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.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 Matrix.toLin' lapMatrix Ring.toAddGroupWithOne Real.instRing Real.semiring Submodule.addCommMonoid Submodule.module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range ConnectedComponent lapMatrix_ker_basis_aux	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Submodule.mem_span_range_iff_exists_fun lapMatrix_mulVec_eq_zero_iff_forall_reachable Matrix.toLin'_apply LinearMap.map_coe_ker mem_ker_toLin'_lapMatrix_of_connectedComponent Finset.sum_congr AddSubmonoid.coe_finset_sum Finset.sum_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq

---

← Back to Index