Theorem LinearIndependent.cardinal_le_rank'

Modification history

2024-01-01 14:48

Mathlib/LinearAlgebra/Dimension.lean

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

Modified LinearIndependent.cardinal_le_rank'View on Github →

2023-12-27 04:42

Mathlib/LinearAlgebra/Dimension.lean

chore(LinearAlgebra): rename to enable `LinearIndependent` dot notation (#9144) …

Added LinearIndependent.cardinal_le_rank'View on Github →