Commit 2025-03-31 13:41 de42deaf

View on Github →

chore(Dimension/Finrank): golf, reuse variables (#23232)

Estimated changes

modified theorem LinearEquiv.finrank_eq
modified theorem LinearEquiv.finrank_map_eq