Theorem DirectSum.component.of

Modification history

2024-08-08 02:10

Mathlib/Algebra/DirectSum/Module.lean

chore: backports for leanprover/lean4#4814 (part 32) (#15577)

Modified DirectSum.component.of View on Github →

2023-03-17 16:27

Mathlib/Algebra/DirectSum/Module.lean

feat: port Algebra.DirectSum.Module (#2596)

Added DirectSum.component.of View on Github →