Theorems · Theorem · combinatorics
SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux
∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
[inst_3 : DecidableEq G.ConnectedComponent], ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites33
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Top.topstatement and proof · cited by 9,680
- Fintypestatement and proof · cited by 7,736
- Submodulestatement · cited by 7,192
- Set.rangestatement · cited by 4,705
- Matrixstatement · cited by 4,303
- mul_oneproof · cited by 3,885
- Finset.univproof · cited by 3,473
- LinearEquivstatement · cited by 3,317
Cited by1
Results whose statement or proof uses this declaration.
- SimpleGraph.lapMatrix_ker_basisproof · cited by 1