From 8ae07ffb75c33dba7c313fa6bd94c243c6ed5fe2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Tue, 10 Dec 2024 12:28:31 +0100 Subject: [PATCH 1/2] docs(LinearAlgebra/InvariantBasisNumber): first letter of a sentence capital --- Mathlib/LinearAlgebra/InvariantBasisNumber.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean index 2979de0ca709c..9632b28faeff2 100644 --- a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean +++ b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean @@ -24,10 +24,10 @@ Let `R` be a (not necessary commutative) ring. It is also useful to consider the following stronger conditions: -- the *rank condition*, witnessed by the type class `RankCondition R`, states that +- The *rank condition*, witnessed by the type class `RankCondition R`, states that the existence of a surjective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `m ≤ n` -- the *strong rank condition*, witnessed by the type class `StrongRankCondition R`, states +- The *strong rank condition*, witnessed by the type class `StrongRankCondition R`, states that the existence of an injective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `n ≤ m`. From 4a067e5d26857fca7e648466e56b9d8e234f364f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Tue, 10 Dec 2024 15:56:22 +0100 Subject: [PATCH 2/2] Update Mathlib/LinearAlgebra/InvariantBasisNumber.lean Co-authored-by: Jz Pan --- Mathlib/LinearAlgebra/InvariantBasisNumber.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean index 9632b28faeff2..fd7f09efc5db7 100644 --- a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean +++ b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean @@ -25,7 +25,7 @@ Let `R` be a (not necessary commutative) ring. It is also useful to consider the following stronger conditions: - The *rank condition*, witnessed by the type class `RankCondition R`, states that - the existence of a surjective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `m ≤ n` + the existence of a surjective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `m ≤ n`. - The *strong rank condition*, witnessed by the type class `StrongRankCondition R`, states that the existence of an injective linear map `(Fin n → R) →ₗ[R] (Fin m → R)`