mathlib

4111ed94 - docs(linear_algebra/invariant_basis_number): Drop a TODO (#14973)

docs(linear_algebra/invariant_basis_number): Drop a TODO (#14973) This TODO was fixed some time ago by @riccardobrasca, reference the relevant instance in the docstring.