Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-30 01:16 a3ba4d47

View on Github →

feat(algebra/homology): eval and forget functors (#7742) From LTE.

Estimated changes

Modified src/algebra/homology/additive.lean

Modified src/algebra/homology/differential_object.lean

Modified src/algebra/homology/homological_complex.lean

added def homological_complex.eval

deleted def homological_complex.eval_at

added def homological_complex.forget

added def homological_complex.forget_eval

Modified src/category_theory/graded_object.lean

added def category_theory.graded_object.eval