Mathlib Changelog v4

Changelog About Github

Theorem DirectSum.add_apply

Modification history

2023-01-30 11:13

Mathlib/Algebra/DirectSum/Basic.lean

feat: port Algebra.DirectSum.Basic (#1923) …

Added DirectSum.add_apply View on Github →