Theorem FiniteDimensional.finrank_eq_card_basis'

Modification history

2024-10-03 19:18

Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

chore: Rename `FiniteDimensional.finrank` to `Module.finrank` (#17192) …

Deleted FiniteDimensional.finrank_eq_card_basis'View on Github →

2024-07-15 10:14

Mathlib/LinearAlgebra/FiniteDimensional.lean

chore: split LinearAlgebra.FiniteDimensional (#14670) …

Modified FiniteDimensional.finrank_eq_card_basis'View on Github →

2023-04-25 11:42

Mathlib/LinearAlgebra/FiniteDimensional.lean

feat: port LinearAlgebra.FiniteDimensional (#3466)

Added FiniteDimensional.finrank_eq_card_basis'View on Github →