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
.