[Merged by Bors] - feat(AlgebraicTopology/SimplicialSet): induction principles for nondegenerate simplices#37335

joelriou wants to merge 8 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

joelriou:nondegenerate-simplices-inductionjoelriou/mathlib4:nondegenerate-simplices-inductionCopy head branch name to clipboard