mathlib

dc1b045a - feat(linear_algebra/free_module/strong_rank_condition): add `comm_ring_strong_rank_condition` (#9486)

feat(linear_algebra/free_module/strong_rank_condition): add `comm_ring_strong_rank_condition` (#9486) We add `comm_ring_strong_rank_condition`: any commutative ring satisfies the strong rank condition. Because of a circular import, this can't be in `linear_algebra.invariant_basis_number`.