Commit 2024-08-04 10:58 64580bf1

View on Github →

chore: Address todo in Data/Matrix/Rank.lean (#15191) This PR addresses a todo in Data/Matrix/Rank.lean, generalizing from LinearOrderedField to Field as suggested by this old Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/row.20rank.20equals.20column.20rank/near/350462992

Estimated changes

Modified Mathlib/Data/Matrix/Rank.lean

modified theorem Matrix.rank_eq_finrank_span_row

modified theorem Matrix.rank_self_mul_transpose

modified theorem Matrix.rank_transpose