Theorem rank_directSum

Modification history

2025-01-20 13:22

Mathlib/LinearAlgebra/Dimension/Constructions.lean

chore(LinearAlgebra): generalize results on ranks to semirings (#20774)

Modified rank_directSum View on Github →

2024-01-01 14:48

Mathlib/LinearAlgebra/Dimension/Constructions.lean

chore: Reorganize results about `rank` and `finrank`. (#9349) …

Modified rank_directSum View on Github →

2023-04-14 14:34

Mathlib/LinearAlgebra/FreeModule/Rank.lean

feat: port LinearAlgebra.FreeModule.Rank (#3377) …

Added rank_directSum View on Github →