Commit 2025-10-07 20:49 d88ac22d

View on Github →

feat(Combinatorics/Quiver): add strongly connected quivers (#29754) Define strongly connected quivers and their components. Add both standard strong connectivity (allowing length-0 paths) and positive-path strong connectivity. Establish basic properties and relationships to weak connectivity via symmetrification. This is part of Perron Frobenius theorem and grounds its characterization/def of Irreducible matrices and Markov chain analysis in subsequent PRs. split from #28728

Estimated changes

Modified Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

added theorem Quiver.IsSStronglyConnected.exists_pos_cycle

added theorem Quiver.IsSStronglyConnected.exists_pos_path

added theorem Quiver.IsSStronglyConnected.isStronglyConnected

added def Quiver.IsSStronglyConnected

added theorem Quiver.IsStronglyConnected.isSStronglyConnected_of_hom

added theorem Quiver.IsStronglyConnected.isStronglyConnected_symmetrify

added theorem Quiver.IsStronglyConnected.nonempty_path

added def Quiver.IsStronglyConnected

added theorem Quiver.StronglyConnectedComponent.IsSStronglyConnected.pos_cycle

added theorem Quiver.StronglyConnectedComponent.mk_eq_mk

added def Quiver.StronglyConnectedComponent

added theorem Quiver.exists_path_of_stronglyConnectedComponent_eq

added theorem Quiver.isSStronglyConnected_iff

added theorem Quiver.isStronglyConnected_iff

added theorem Quiver.stronglyConnectedComponent_eq_of_path

added theorem Quiver.stronglyConnectedComponent_singleton_iff

added def Quiver.stronglyConnectedSetoid

Modified Mathlib/Combinatorics/Quiver/Symmetric.lean

deleted def Quiver.IsPreconnected