Commit 2021-09-23 16:42 9e367ffb

feat(linear_algebra/invariant_basis_number): strong_rank_condition_iff_succ (#9128) We add strong_rank_condition_iff_succ: a ring satisfies the strong rank condition if and only if, for all n : ℕ, there are no injective linear maps (fin (n + 1) → R) →ₗ[R] (fin n → R). This will be used to prove that any commutative ring satisfies the strong rank condition. The proof is simple and it uses the natural inclusion R^n → R^m, for n ≤ m (adding zeros at the end). We provide this in general as extend_by_zero.linear_map : (ι → R) →ₗ[R] (η → R) where ι and η are types endowed with a function ι → η.