Theorem CategoryTheory.HasShift.Induced.add_inv_app_obj

Modification history

2023-09-04 15:04
Mathlib/CategoryTheory/Shift/Induced.lean
feat: the induced shift on the target category of a functor (#6652) …
Added CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-18 09:39
Mathlib/CategoryTheory/Shift/Induced.lean
trying to revert unwanted commits
Deleted CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-18 09:18
Mathlib/CategoryTheory/Shift/Induced.lean
Merge remote-tracking branch 'origin/shift_induced'
Added CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-17 11:16
Mathlib/CategoryTheory/Shift/Induced.lean
refactor(Algebra/Lie/BaseChange): use new tensor product machinery (#6628)
Deleted CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-17 15:45
Mathlib/CategoryTheory/Shift/Induced.lean
pleasing the linter
Added CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-17 10:19
Mathlib/CategoryTheory/Shift/Induced.lean
fix: patch for std4#193 (#6188) …
Deleted CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →
2023-08-17 15:19
Mathlib/CategoryTheory/Shift/Induced.lean
feat: the induced shift on the target category of a functor
Added CategoryTheory.HasShift.Induced.add_inv_app_objView on Github →