Theorem DirectSum.induction_lon

Modification history

2025-04-30 12:59
Mathlib/LinearAlgebra/FreeProduct/Basic.lean
style: further whitespace fixes (#24467) …
Modified DirectSum.induction_lonView on Github →
2024-07-19 14:02
Mathlib/LinearAlgebra/FreeProduct/Basic.lean
feat (LinearAlgebra/FreeProduct): introduce basic structure, universal property (#14858) …
Added DirectSum.induction_lonView on Github →