Mathlib: HasFiniteBiproducts on a Serre full subcategory isn't found via Abelian

For P : ObjectProperty C with P.IsSerreClass (or closed under finite products) in an abelian C, inferInstance : Abelian P.FullSubcategory works, but a class like IsKrullSchmidt P.FullSubcategory that takes [Preadditive] [HasFiniteBiproducts] as parameters fails to find HasFiniteBiproducts. The one derived from Abelian goes through Abelian.toPreadditive, a different instance path from the full subcategory's own Preadditive. Fix: instance : HasFiniteBiproducts P.FullSubcategory := .of_hasFiniteProducts, which uses HasFiniteProducts from IsClosedUnderFiniteProducts. Endomorphism rings transfer with a RingEquiv built from P.fullyFaithfulι.mulEquivEnd X plus map_add' := by ext; simp only [Functor.FullyFaithful.mulEquivEnd]; exact P.ι.map_add.