OAI/Topology/ArtinGroups/Harmonic/EigenvectorProportional.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.HarmonicArtin.GraphConnection.eigenvector_proportionalline 11 - theorem
OAI.HarmonicArtin.GraphConnection.nonnegative_eigenvector_proportionalline 45