Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 08:10 dc1b045a

View on Github →

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.

Estimated changes