ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>rTensor.inverse Q hfg hg ∘ₗ LinearMap.rTensor Q g = (LinearMap.range (LinearMap.rTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>N : Submodule R M<GOAL>LinearMap.ker (LinearMap.rTensor Q N.mkQ) = LinearMap.range (LinearMap.rTensor Q N.subtype)
<VAR>R : Type u_1<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R N<VAR>Module R P<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>AddCommGroup N'<VAR>AddCommGroup P'<VAR>Module R N'<VAR>Module R P'<VAR>g' : N' →ₗ[R] P'<VAR>hg' : Function.Surjective ⇑g'<GOAL>Function.Surjective ⇑(TensorProduct.map g g')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>AddCommGroup M'<VAR>AddCommGroup N'<VAR>AddCommGroup P'<VAR>Module R M'<VAR>Module R N'<VAR>Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Function.Exact ⇑f' ⇑g'<VAR>hg' : Function.Surjective ⇑g'<GOAL>LinearMap.ker (TensorProduct.map g g') = LinearMap.range (LinearMap.lTensor N f') ⊔ LinearMap.range (LinearMap.rTensor N' f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Type u_9<VAR>Semiring S<VAR>Algebra R S<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>Function.Surjective ⇑((TensorProduct.mk R S M) 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>r : R<VAR>x : M<GOAL>(quotTensorEquivQuotSMul M I) ((Ideal.Quotient.mk I) r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(quotTensorEquivQuotSMul M I) ∘ₗ LinearMap.rTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.lid R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>x : M<GOAL>(quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(quotTensorEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (TensorProduct.mk R (R ⧸ I) M) 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(quotTensorEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R (R ⧸ I) M) 1 = (I • ⊤).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>x : M<VAR>r : R<GOAL>(tensorQuotEquivQuotSMul M I) (x ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(tensorQuotEquivQuotSMul M I) ∘ₗ LinearMap.lTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.rid R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>x : M<GOAL>(tensorQuotEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = x ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(tensorQuotEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (TensorProduct.mk R M (R ⧸ I)).flip 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>↑(tensorQuotEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R M (R ⧸ I)).flip 1 = (I • ⊤).mkQ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal A<GOAL>Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeLeft I) = LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>I : Ideal B<GOAL>Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeRight I) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)
<VAR>R : Type u_4<VAR>CommRing R<VAR>A : Type u_5<VAR>C : Type u_7<VAR>D : Type u_8<VAR>Ring A<VAR>Ring C<VAR>Ring D<VAR>Algebra R A<VAR>Algebra R C<VAR>Algebra R D<VAR>g : C →ₐ[R] D<VAR>hg : Function.Surjective ⇑g<GOAL>RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
<VAR>R : Type u_4<VAR>CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)
<VAR>R : Type u_4<VAR>CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>Ring A<VAR>Ring B<VAR>Ring C<VAR>Ring D<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔ Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>m : M<GOAL>(ExteriorAlgebra.GradedAlgebra.ι R M) m = (DirectSum.of (fun i => ↥(⋀[R]^i M)) 1) ⟨(ExteriorAlgebra.ι R) m, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>m : M<GOAL>(ExteriorAlgebra.GradedAlgebra.ι R M) m * (ExteriorAlgebra.GradedAlgebra.ι R M) m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>i : ℕ<VAR>x : ↥(⋀[R]^i M)<GOAL>(ExteriorAlgebra.GradedAlgebra.liftι R M) ↑x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Submodule.span R (Set.range fun x => (ExteriorAlgebra.ιMulti R x.fst) x.snd) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : Submodule.span R Φ = ⊤<VAR>e : M ≃ₗ[R] M<VAR>he : Set.MapsTo (⇑e) Φ Φ<GOAL>IsOfFinOrder e
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.rank R M = ⨆ ι, #↑↑ι
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.rank R M ≤ #M
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Nonempty { s // 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>Nontrivial R<VAR>ι : Type w<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>Cardinal.lift.{v, w} #ι ≤ Cardinal.lift.{w, v} (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>ι : Type w<VAR>Infinite ι<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>ℵ₀ ≤ 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>ι : Type v<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>#ι ≤ 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>s : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<GOAL>#↑s ≤ Module.rank R M
<VAR>R : Type u<VAR>R' : Type u'<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R' M'<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : Function.Injective ⇑j<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R' M'<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Function.Surjective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R' M'<VAR>i : ZeroHom R R'<VAR>j : M ≃+ M'<VAR>hi : Function.Bijective ⇑i<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R' M₁<VAR>i : R' → R<VAR>j : M →+ M₁<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : Function.Injective ⇑j<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>Module.rank R M ≤ Module.rank R' M₁
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M₁<VAR>hi : Function.Surjective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Module.rank R M ≤ Module.rank R' M₁
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>Ring R<VAR>Ring R'<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M ≃+ M₁<VAR>hi : Function.Bijective ⇑i<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Module.rank R M = Module.rank R' M₁
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Function.Injective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<GOAL>Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Function.Surjective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<GOAL>Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<GOAL>Cardinal.lift.{v', v} (Module.rank R S) = Cardinal.lift.{v, v'} (Module.rank R' S')
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R' →+* R<VAR>j : S →+* S'<VAR>hi : Function.Injective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'<GOAL>Module.rank R S ≤ Module.rank R' S'
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Function.Surjective ⇑i<VAR>hj : Function.Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<GOAL>Module.rank R S ≤ Module.rank R' S'
<VAR>R : Type w<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>R' : Type w'<VAR>S' : Type v<VAR>CommRing R'<VAR>Ring S'<VAR>Algebra R' S'<VAR>i : R ≃+* R'<VAR>j : S ≃+* S'<VAR>hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)<GOAL>Module.rank R S = Module.rank R' S'
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>i : Function.Injective ⇑f<GOAL>Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>i : Function.Injective ⇑f<GOAL>Module.rank R M ≤ Module.rank R M₁
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<GOAL>Cardinal.lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) ≤ Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<GOAL>Module.rank R ↥(LinearMap.range f) ≤ Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>p : Submodule R M<GOAL>Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ Cardinal.lift.{v', v} (Module.rank R ↥p)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<GOAL>Module.rank R ↥(Submodule.map f p) ≤ Module.rank R ↥p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s t : Submodule R M<VAR>h : s ≤ t<GOAL>Module.rank R ↥s ≤ Module.rank R ↥t
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M ≃ₗ[R] M'<GOAL>Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M ≃ₗ[R] M₁<GOAL>Module.rank R M = Module.rank R M₁
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>h : Function.Injective ⇑f<GOAL>Cardinal.lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>h : Function.Injective ⇑f<GOAL>Module.rank R ↥(LinearMap.range f) = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M ≃ₗ[R] M'<VAR>p : Submodule R M<GOAL>Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map (↑f) p)) = Cardinal.lift.{v', v} (Module.rank R ↥p)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M ≃ₗ[R] M₁<VAR>p : Submodule R M<GOAL>Module.rank R ↥(Submodule.map (↑f) p) = Module.rank R ↥p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.rank R ↥⊤ = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>h : Function.Surjective ⇑f<GOAL>Module.rank R ↥(LinearMap.range f) = Module.rank R M'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Submodule R M<GOAL>Module.rank R ↥s ≤ Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>h : Function.Surjective ⇑f<GOAL>Cardinal.lift.{v, v'} (Module.rank R M') ≤ Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>h : Function.Surjective ⇑f<GOAL>Module.rank R M₁ ≤ Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Subsingleton R<GOAL>Module.rank R M = 1
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>P : K[X]<VAR>k : ℕ<VAR>sep : P.Separable<VAR>nil : minpoly K f ∣ P ^ k<GOAL>∃ n ∈ Algebra.adjoin K {f}, ∃ s ∈ Algebra.adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : Module.End K V<VAR>PerfectField K<GOAL>∃ n ∈ Algebra.adjoin K {f}, ∃ s ∈ Algebra.adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>DecidableEq n<VAR>d : n → R<GOAL>(Matrix.diagonal d).PosSemidef ↔ ∀ (i : n), 0 ≤ d i
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<GOAL>M.IsHermitian
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosSemidef<VAR>x : n → 𝕜<GOAL>0 ≤ RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>A : Matrix n n R<VAR>hA : A.PosSemidef<VAR>m : Type u_5<VAR>Fintype m<VAR>B : Matrix n m R<GOAL>(B.conjTranspose * A * B).PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>A : Matrix n n R<VAR>hA : A.PosSemidef<VAR>m : Type u_5<VAR>Fintype m<VAR>B : Matrix m n R<GOAL>(B * A * B.conjTranspose).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype m<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>e : m → n<GOAL>(M.submatrix e e).PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<GOAL>M.transpose.PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<GOAL>M.conjTranspose.PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<GOAL>Matrix.PosSemidef 0
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>DecidableEq n<GOAL>Matrix.PosSemidef 1
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>k : ℕ<GOAL>(M ^ k).PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<GOAL>M⁻¹.PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>DecidableEq n<VAR>M : Matrix n n R<VAR>hM : M.PosSemidef<VAR>z : ℤ<GOAL>(M ^ z).PosSemidef
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>Fintype m<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosSemidef<GOAL>(A + B).PosSemidef
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>i : n<GOAL>0 ≤ ⋯.eigenvalues i
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<GOAL>hA.sqrt.PosSemidef
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<GOAL>hA.sqrt ^ 2 = A
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<GOAL>hA.sqrt * hA.sqrt = A
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B ^ 2<GOAL>A = B
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<GOAL>(⋯ : (A ^ 2).PosSemidef).sqrt = A
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>B : Matrix n n 𝕜<VAR>hB : B.PosSemidef<VAR>hAB : A ^ 2 = B<GOAL>A = hB.sqrt
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype m<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>e : m ≃ n<GOAL>(M.submatrix ⇑e ⇑e).PosSemidef ↔ M.PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype m<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(A.conjTranspose * A).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype m<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(A * A.conjTranspose).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>RCLike 𝕜<VAR>A : Matrix m n 𝕜<VAR>DecidableEq n<VAR>i : n<GOAL>0 ≤ ⋯.eigenvalues i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype m<VAR>Fintype n<VAR>RCLike 𝕜<VAR>A : Matrix m n 𝕜<VAR>DecidableEq m<VAR>i : m<GOAL>0 ≤ ⋯.eigenvalues i
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>A : Matrix n n 𝕜<GOAL>A.PosSemidef ↔ ∃ B, A = B.conjTranspose * B
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h : ∀ (i : n), 0 ≤ hA.eigenvalues i<GOAL>A.PosSemidef
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>x : n → 𝕜<GOAL>Matrix.dotProduct (star x) (A.mulVec x) = 0 ↔ A.mulVec x = 0
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>x : n → 𝕜<GOAL>(((Matrix.toLinearMap₂' 𝕜) A) (star x)) x = 0 ↔ (Matrix.toLin' A) x = 0
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>M.IsHermitian
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<VAR>x : n → 𝕜<VAR>hx : x ≠ 0<GOAL>0 < RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>M.PosSemidef
<VAR>n : Type u_2<VAR>R : Type u_3<VAR>Fintype n<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>M : Matrix n n R<VAR>hM : M.PosDef<GOAL>M.transpose.PosDef
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>Fintype m<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A B : Matrix m m R<VAR>hA : A.PosDef<VAR>hB : B.PosSemidef<GOAL>(A + B).PosDef
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>Fintype m<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosDef<GOAL>(A + B).PosDef
<VAR>m : Type u_1<VAR>R : Type u_3<VAR>Fintype m<VAR>CommRing R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A B : Matrix m m R<VAR>hA : A.PosDef<VAR>hB : B.PosDef<GOAL>(A + B).PosDef
<VAR>n : Type u_2<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.IsSymm<VAR>hMq : M.toQuadraticMap'.PosDef<GOAL>M.PosDef
<VAR>n : Type u_2<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n ℝ<VAR>hM : M.PosDef<GOAL>M.toQuadraticMap'.PosDef