Theorem SSet.ι₁_app_snd_apply

Modification history

2026-03-27 09:21
Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean
feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by a homotopy (#33683) …
Added SSet.ι₁_app_snd_applyView on Github →