Theorem RingHom.HasFiniteProducts.preservesFiniteProducts_pushout

Modification history

2026-05-24 17:27
Mathlib/Algebra/Category/Ring/Under/Property.lean
feat(Algebra/Category/Ring): `Under.pushout` preserves finite limits for properties with stable equalizers (#39572) …
Added RingHom.HasFiniteProducts.preservesFiniteProducts_pushoutView on Github →