ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDomain R<VAR>M' : Submodule R M<GOAL>Module.rank R (M ⧸ M') + Module.rank R ↥M' = Module.rank R M
<VAR>R : Type u_1<VAR>Ring R<VAR>IsDomain R<VAR>hS : IsEmpty (OreLocalization.OreSet R⁰)<GOAL>ℵ₀ ≤ Module.rank R R
<VAR>R : Type u_1<VAR>Ring R<VAR>IsDomain R<VAR>StrongRankCondition R<GOAL>Nonempty (OreLocalization.OreSet R⁰)
<VAR>κ : Type uκ<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis κ R M<VAR>i : κ<GOAL>(TensorAlgebra.equivFreeAlgebra b) ((TensorAlgebra.ι R) (b i)) = FreeAlgebra.ι R i
<VAR>κ : Type uκ<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis κ R M<VAR>i : κ<GOAL>(TensorAlgebra.equivFreeAlgebra b).symm (FreeAlgebra.ι R i) = (TensorAlgebra.ι R) (b i)
<VAR>κ : Type uκ<VAR>R : Type uR<VAR>M : Type uM<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis κ R M<GOAL>∀ (a : TensorAlgebra R M), b.tensorAlgebra.repr a = (FreeAlgebra.basisFreeMonoid R κ).repr ((TensorAlgebra.equivFreeAlgebra b) a)
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>Module.Free R M<GOAL>Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (Cardinal.sum fun n => Module.rank R M ^ n)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq l<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix l m α<VAR>D : Matrix l n α<VAR>Invertible A<GOAL>Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 0 (C * ⅟A) 1 * Matrix.fromBlocks A 0 0 (D - C * ⅟A * B) * Matrix.fromBlocks 1 (⅟A * B) 0 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype l<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq l<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix l m α<VAR>B : Matrix l n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible D<GOAL>Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 (B * ⅟D) 0 1 * Matrix.fromBlocks (A - B * ⅟D * C) 0 0 D * Matrix.fromBlocks 1 0 (⅟D * C) 1
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>D : Matrix n n α<VAR>Invertible A<VAR>Invertible D<VAR>Invertible (Matrix.fromBlocks A B 0 D)<GOAL>⅟(Matrix.fromBlocks A B 0 D) = Matrix.fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible A<VAR>Invertible D<VAR>Invertible (Matrix.fromBlocks A 0 C D)<GOAL>⅟(Matrix.fromBlocks A 0 C D) = Matrix.fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>D : Matrix n n α<GOAL>IsUnit (Matrix.fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>IsUnit (Matrix.fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>D : Matrix n n α<VAR>hAD : IsUnit A ↔ IsUnit D<GOAL>(Matrix.fromBlocks A B 0 D)⁻¹ = Matrix.fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>hAD : IsUnit A ↔ IsUnit D<GOAL>(Matrix.fromBlocks A 0 C D)⁻¹ = Matrix.fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible D<VAR>Invertible (A - B * ⅟D * C)<VAR>Invertible (Matrix.fromBlocks A B C D)<GOAL>⅟(Matrix.fromBlocks A B C D) = Matrix.fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C))) (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible A<VAR>Invertible (D - C * ⅟A * B)<VAR>Invertible (Matrix.fromBlocks A B C D)<GOAL>⅟(Matrix.fromBlocks A B C D) = Matrix.fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B))) (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible D<GOAL>IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible A<GOAL>IsUnit (Matrix.fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible A<GOAL>(Matrix.fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<GOAL>(Matrix.fromBlocks 1 B C D).det = (D - C * B).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>Invertible D<GOAL>(Matrix.fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<GOAL>(Matrix.fromBlocks A B C 1).det = (A - B * C).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<GOAL>(1 + A * B).det = (1 + B * A).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<GOAL>(A * B + 1).det = (B * A + 1).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<GOAL>(1 - A * B).det = (1 - B * A).det
<VAR>m : Type u_2<VAR>α : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>ι : Type u_5<VAR>Unique ι<VAR>u v : m → α<GOAL>(1 + Matrix.col ι u * Matrix.row ι v).det = 1 + Matrix.dotProduct v u
<VAR>m : Type u_2<VAR>α : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>CommRing α<VAR>ι : Type u_5<VAR>Unique ι<VAR>A : Matrix m m α<VAR>hA : IsUnit A.det<VAR>u v : m → α<GOAL>(A + Matrix.col ι u * Matrix.row ι v).det = A.det * (1 + Matrix.row ι v * A⁻¹ * Matrix.col ι u).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>A : Matrix m m α<VAR>U : Matrix m n α<VAR>V : Matrix n m α<VAR>hA : IsUnit A.det<GOAL>(A + U * V).det = A.det * (1 + V * A⁻¹ * U).det
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>PartialOrder 𝕜<VAR>StarRing 𝕜<VAR>StarOrderedRing 𝕜<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>Invertible A<VAR>hA : A.IsHermitian<GOAL>Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star (x + (A⁻¹ * B).mulVec y)) A) (x + (A⁻¹ * B).mulVec y) + Matrix.dotProduct (Matrix.vecMul (star y) (D - B.conjTranspose * A⁻¹ * B)) y
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>PartialOrder 𝕜<VAR>StarRing 𝕜<VAR>StarOrderedRing 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>Invertible D<VAR>hD : D.IsHermitian<GOAL>Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D) ((D⁻¹ * B.conjTranspose).mulVec x + y) + Matrix.dotProduct (Matrix.vecMul (star x) (A - B * D⁻¹ * B.conjTranspose)) x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>StarRing 𝕜<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.IsHermitian<GOAL>(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>StarRing 𝕜<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.IsHermitian<GOAL>(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>PartialOrder 𝕜<VAR>StarRing 𝕜<VAR>StarOrderedRing 𝕜<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>Invertible A<GOAL>(Matrix.fromBlocks A B B.conjTranspose D).PosSemidef ↔ (D - B.conjTranspose * A⁻¹ * B).PosSemidef
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>𝕜 : Type u_5<VAR>CommRing 𝕜<VAR>PartialOrder 𝕜<VAR>StarRing 𝕜<VAR>StarOrderedRing 𝕜<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.PosDef<VAR>Invertible D<GOAL>(Matrix.fromBlocks A B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>Semiring S<VAR>Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₂ : ι₂ → Type w₂<VAR>(i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>(i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>(i₁ : ι₁) → Module R (M₁ i₁)<VAR>(i₂ : ι₂) → Module R (M₂ i₂)<VAR>(i₁ : ι₁) → Module S (M₁ i₁)<VAR>∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i₁ : ι₁<VAR>m₁ : M₁ i₁<VAR>i₂ : ι₂<VAR>m₂ : M₂ i₂<GOAL>(TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) = (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>Semiring S<VAR>Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₂ : ι₂ → Type w₂<VAR>(i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>(i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>(i₁ : ι₁) → Module R (M₁ i₁)<VAR>(i₂ : ι₂) → Module R (M₂ i₂)<VAR>(i₁ : ι₁) → Module S (M₁ i₁)<VAR>∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i₁ : ι₁<VAR>m₁ : M₁ i₁<VAR>i₂ : ι₂<VAR>m₂ : M₂ i₂<GOAL>(TensorProduct.directSum R S M₁ M₂).symm ((DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι₁ : Type v₁<VAR>DecidableEq ι₁<VAR>M₁ : ι₁ → Type w₁<VAR>M₂' : Type w₂'<VAR>(i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>AddCommMonoid M₂'<VAR>(i₁ : ι₁) → Module R (M₁ i₁)<VAR>Module R M₂'<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>(TensorProduct.directSumLeft R M₁ M₂') ((DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y) = (DirectSum.lof R ι₁ (fun i => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι₁ : Type v₁<VAR>DecidableEq ι₁<VAR>M₁ : ι₁ → Type w₁<VAR>M₂' : Type w₂'<VAR>(i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>AddCommMonoid M₂'<VAR>(i₁ : ι₁) → Module R (M₁ i₁)<VAR>Module R M₂'<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>(TensorProduct.directSumLeft R M₁ M₂').symm ((DirectSum.lof R ι₁ (fun i => TensorProduct R (M₁ i) M₂') i) (x ⊗ₜ[R] y)) = (DirectSum.lof R ι₁ M₁ i) x ⊗ₜ[R] y
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι₂ : Type v₂<VAR>DecidableEq ι₂<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>AddCommMonoid M₁'<VAR>(i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>Module R M₁'<VAR>(i₂ : ι₂) → Module R (M₂ i₂)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(TensorProduct.directSumRight R M₁' M₂) (x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y) = (DirectSum.lof R ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>CommSemiring R<VAR>ι₂ : Type v₂<VAR>DecidableEq ι₂<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>AddCommMonoid M₁'<VAR>(i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>Module R M₁'<VAR>(i₂ : ι₂) → Module R (M₂ i₂)<VAR>x : M₁'<VAR>i : ι₂<VAR>y : M₂ i<GOAL>(TensorProduct.directSumRight R M₁' M₂).symm ((DirectSum.lof R ι₂ (fun i => TensorProduct R M₁' (M₂ i)) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i) y
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<GOAL>Module.rank R M ≤ ↑n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.rank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<GOAL>Module.rank R M = 0 ↔ ∀ (x : M), x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<GOAL>Module.rank R M = 0 ↔ Subsingleton M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<GOAL>0 < Module.rank R M ↔ ∃ x, x ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<GOAL>0 < Module.rank R M ↔ Nontrivial M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.rank R M = 0 ↔ Module.IsTorsion R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>Nontrivial M<GOAL>0 < Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>Subsingleton M<GOAL>Module.rank R M = 0
<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<GOAL>Module.rank R PUnit.{u_1 + 1} = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<GOAL>Module.rank R ↥⊥ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>s : Submodule R M<VAR>h : 0 < Module.rank R ↥s<GOAL>∃ b ∈ s, b ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>n : ℕ<VAR>h : Module.rank R M = ↑n<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>h : Module.rank R M = 0<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : Module.rank R M = 1<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>h : Module.rank R M < ℵ₀<GOAL>Nonempty (Fintype ι)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>s : Set ι<VAR>b : Basis (↑s) R M<VAR>h : Module.rank R M < ℵ₀<GOAL>s.Finite
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>ι : Type w<VAR>b : ι → M<VAR>h : LinearIndependent R b<GOAL>#ι ≤ ↑(FiniteDimensional.finrank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>ι : Type u_1<VAR>Fintype ι<VAR>b : ι → M<VAR>h : LinearIndependent R b<GOAL>Fintype.card ι ≤ FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>b : Finset M<VAR>h : LinearIndependent R fun x => ↑x<GOAL>b.card ≤ FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>Module.Finite R M<VAR>v : ι → M<VAR>h : LinearIndependent R v<GOAL>#ι < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>ι : Type u_1<VAR>f : ι → M<VAR>h : LinearIndependent R f<GOAL>Finite ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>b : Set M<VAR>h : LinearIndependent R fun (x : ↑b) => ↑x<GOAL>b.Finite
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : Cardinal.{v}<VAR>hn : n < Module.rank R M<GOAL>∃ s, #↑s = n ∧ LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>hn : ↑n ≤ Module.rank R M<GOAL>∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>hn : ↑n ≤ Module.rank R M<GOAL>∃ f, LinearIndependent R f
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>n : ℕ<GOAL>↑n ≤ Module.rank R M ↔ ∃ f, LinearIndependent R f
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>n : ℕ<GOAL>↑n ≤ Module.rank R M ↔ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>hn : n ≤ FiniteDimensional.finrank R M<GOAL>∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>hn : n ≤ FiniteDimensional.finrank R M<GOAL>∃ f, LinearIndependent R f
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>ι : Type u_1<VAR>Infinite ι<VAR>v : ι → M<GOAL>¬LinearIndependent R v
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>Nontrivial R<VAR>V : ι → Submodule R M<VAR>hV : CompleteLattice.Independent V<GOAL>Cardinal.lift.{v, w} #{ i // V i ≠ ⊥ } ≤ Cardinal.lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<VAR>p : ι → Submodule R M<VAR>hp : CompleteLattice.Independent p<GOAL>#{ i // p i ≠ ⊥ } ≤ ↑(FiniteDimensional.finrank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<VAR>p : ι → Submodule R M<VAR>hp : CompleteLattice.Independent p<VAR>Fintype { i // p i ≠ ⊥ }<GOAL>Fintype.card { i // p i ≠ ⊥ } ≤ FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>t : Finset M<VAR>h : FiniteDimensional.finrank R M < t.card<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>t : Finset M<VAR>h : FiniteDimensional.finrank R M + 1 < t.card<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>h : 0 < FiniteDimensional.finrank R M<GOAL>Nontrivial M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank R M = n.succ<GOAL>Nontrivial M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>Subsingleton M<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_1<VAR>Nontrivial R<VAR>Infinite ι<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<GOAL>FiniteDimensional.finrank R ↥⊥ = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<GOAL>0 < FiniteDimensional.finrank R M ↔ ∃ x, x ≠ 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<GOAL>0 < FiniteDimensional.finrank R M ↔ Nontrivial M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<VAR>h : Nontrivial M<GOAL>0 < FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<GOAL>FiniteDimensional.finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
<VAR>M : Type v<VAR>AddCommGroup M<VAR>R : Type u_1<VAR>CommRing R<VAR>StrongRankCondition R<VAR>IsDomain R<VAR>Module R M<VAR>Module.Finite R M<GOAL>FiniteDimensional.finrank R M = 0 ↔ Module.IsTorsion R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>NoZeroSMulDivisors R M<GOAL>FiniteDimensional.finrank R M = 0 ↔ Subsingleton M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>h : Module.rank R M = 0<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>h : Module.rank R M = 0<GOAL>⊥ = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>NoZeroSMulDivisors R M<VAR>S : Submodule R M<GOAL>Module.rank R ↥S = 0 ↔ S = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>NoZeroSMulDivisors R M<VAR>S : Submodule R M<VAR>Module.Finite R ↥S<GOAL>FiniteDimensional.finrank R ↥S = 0 ↔ S = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>StrongRankCondition R<VAR>NoZeroSMulDivisors R M<VAR>S : Submodule R M<VAR>Module.Finite R ↥S<GOAL>1 ≤ FiniteDimensional.finrank R ↥S ↔ S ≠ ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ∀ (s : Finset M), Basis (↑↑s) R M → False<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ¬∃ s, Nonempty (Basis (↑↑s) R M)<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ¬∃ s x, s.Finite<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)<GOAL>FiniteDimensional.finrank R M = 0