Theorem Pi.mulSingle_induction

Modification history

2025-12-20 21:16
Mathlib/Algebra/BigOperators/Pi.lean
feat(RingTheory/FinitePresentation): a finite product of finitely presented algebras is finitely presented (#32758) …
Modified Pi.mulSingle_inductionView on Github →
2025-01-27 22:45
Mathlib/Algebra/BigOperators/Pi.lean
feat(Algebra): `Pi.single_induction` (#21141) …
Added Pi.mulSingle_inductionView on Github →