Commit 2023-05-17 06:12 4cb84b72

View on Github →

feat: port Algebra.Homology.Opposite (#3998)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Opposite.lean

added def HomologicalComplex.homologyOpDef

added def HomologicalComplex.homologyUnopDef

added def HomologicalComplex.opCounitIso

added def HomologicalComplex.opEquivalence

added def HomologicalComplex.opFunctor

added def HomologicalComplex.opInverse

added def HomologicalComplex.opUnitIso

added def HomologicalComplex.unopCounitIso

added def HomologicalComplex.unopEquivalence

added def HomologicalComplex.unopFunctor

added def HomologicalComplex.unopInverse

added def HomologicalComplex.unopUnitIso

added def homologyOp

added def homologyUnop

added theorem imageToKernel_op

added theorem imageToKernel_unop