Linear

Statistics

Metric	Count
Definitions	0
Theorems `instLinearLocalization'ShiftFunctorOfCommShiftOfQ'`, `instLinearLocalizationShiftFunctorOfCommShiftOfQ`, `linear_of_localization`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`instLinearLocalization'ShiftFunctorOfCommShiftOfQ'` 📖	mathematical	`CategoryTheory.Functor.Linear` `Ring.toSemiring` `CategoryTheory.shiftFunctor`	`CategoryTheory.MorphismProperty.Localization'` `CategoryTheory.MorphismProperty.instCategoryLocalization'`	—	`linear_of_localization` `CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'`
`instLinearLocalizationShiftFunctorOfCommShiftOfQ` 📖	mathematical	`CategoryTheory.Functor.Linear` `Ring.toSemiring` `CategoryTheory.shiftFunctor`	`CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization`	—	`linear_of_localization` `CategoryTheory.Functor.q_isLocalization`
`linear_of_localization` 📖	—	`CategoryTheory.Functor.Linear` `Ring.toSemiring` `CategoryTheory.shiftFunctor`	—	—	`CategoryTheory.Localization.functor_linear_iff` `CategoryTheory.Functor.instLinearComp`

---