Theorem CategoryTheory.DifferentialObject.d_squared_apply

Modification history

2026-09-26 09:19
Mathlib/Algebra/Homology/DifferentialObject.lean
chore: use `congr()` much more widely (#43408) …
Modified CategoryTheory.DifferentialObject.d_squared_applyView on Github →
2024-03-13 20:53
Mathlib/Algebra/Homology/DifferentialObject.lean
chore: remove more autoImplicit (#11336) …
Modified CategoryTheory.DifferentialObject.d_squared_applyView on Github →
2023-06-29 10:11
Mathlib/Algebra/Homology/DifferentialObject.lean
feat: port Algebra.Homology.DifferentialObject (#5033)
Added CategoryTheory.DifferentialObject.d_squared_applyView on Github →