ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>I : Ideal A<VAR>f : A →ₐ[R₁] B<VAR>hI : ∀ a ∈ I, f a = 0<GOAL>(Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>r : R₁<VAR>x : A ⧸ RingHom.ker f<GOAL>f.kerLift (r • x) = r • f.kerLift x
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>a : A<GOAL>(Ideal.kerLiftAlg f) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<GOAL>↑(Ideal.kerLiftAlg f) = (↑f).kerLift
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<GOAL>Function.Injective ⇑(Ideal.kerLiftAlg f)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>g : B → A<VAR>hf : Function.RightInverse g ⇑f<VAR>a : A ⧸ RingHom.ker f.toRingHom<GOAL>(Ideal.quotientKerAlgEquivOfRightInverse hf) a = (↑f).kerLift a
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>g : B → A<VAR>hf : Function.RightInverse g ⇑f<GOAL>∀ (a : B), (Ideal.quotientKerAlgEquivOfRightInverse hf).symm a = (Ideal.Quotient.mk (RingHom.ker ↑f)) (g a)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>hf : Function.Surjective ⇑f<GOAL>∀ (a : B), (Ideal.quotientKerAlgEquivOfSurjective hf).symm a = (Ideal.Quotient.mk (RingHom.ker ↑f)) (Classical.choose ⋯ a)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>f : A →ₐ[R₁] B<VAR>hf : Function.Surjective ⇑f<VAR>a : A ⧸ RingHom.ker f.toRingHom<GOAL>(Ideal.quotientKerAlgEquivOfSurjective hf) a = (↑f).kerLift a
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ Ideal.comap f I<VAR>x : R<GOAL>(Ideal.quotientMap I f H) ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f x)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>S : Type v<VAR>CommRing S<VAR>J : Ideal A<VAR>I : Ideal S<VAR>f : A →+* S<VAR>H : J ≤ Ideal.comap f I<VAR>x : R₁<GOAL>(Ideal.quotientMap I f H) ((algebraMap R₁ (A ⧸ J)) x) = (Ideal.Quotient.mk I) (f ((algebraMap R₁ A) x))
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ Ideal.comap f I<GOAL>(Ideal.quotientMap I f H).comp (Ideal.Quotient.mk J) = (Ideal.Quotient.mk I).comp f
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = Ideal.map (↑f) I<VAR>a : S ⧸ J<GOAL>(I.quotientEquiv J f hIJ).symm a = (Ideal.quotientMap I ↑f.symm ⋯) a
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = Ideal.map (↑f) I<GOAL>∀ (a : R ⧸ I), (I.quotientEquiv J f hIJ) a = (↑↑(Ideal.quotientMap J ↑f ⋯)).toFun a
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = Ideal.map (↑f) I<VAR>x : R<GOAL>(I.quotientEquiv J f hIJ) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) (f x)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>f : R ≃+* S<VAR>hIJ : J = Ideal.map (↑f) I<VAR>x : S<GOAL>(I.quotientEquiv J f hIJ).symm ((Ideal.Quotient.mk J) x) = (Ideal.Quotient.mk I) (f.symm x)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ Ideal.comap f I<VAR>h : Ideal.comap f I ≤ J<GOAL>Function.Injective ⇑(Ideal.quotientMap I f H)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>I : Ideal S<VAR>f : R →+* S<GOAL>Function.Injective ⇑(Ideal.quotientMap I f ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ Ideal.comap f I<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(Ideal.quotientMap I f H)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>R' : Type u_5<VAR>S' : Type u_6<VAR>CommRing R'<VAR>CommRing S'<VAR>f : R →+* S<VAR>f' : R' →+* S'<VAR>g : R →+* R'<VAR>g' : S →+* S'<VAR>hfg : f'.comp g = g'.comp f<VAR>I : Ideal S'<GOAL>let leq := ⋯;
(Ideal.quotientMap I g' ⋯).comp (Ideal.quotientMap (Ideal.comap g' I) f ⋯) = (Ideal.quotientMap I f' ⋯).comp (Ideal.quotientMap (Ideal.comap f' I) g leq)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>CommRing B<VAR>Algebra R₁ B<VAR>I : Ideal A<VAR>J : Ideal B<VAR>f : A →ₐ[R₁] B<VAR>H : I ≤ Ideal.comap f J<VAR>x : A<GOAL>(Ideal.quotientMapₐ J f H) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mkₐ R₁ J) (f x)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>CommRing B<VAR>Algebra R₁ B<VAR>I : Ideal A<VAR>J : Ideal B<VAR>f : A →ₐ[R₁] B<VAR>H : I ≤ Ideal.comap f J<GOAL>(Ideal.quotientMapₐ J f H).comp (Ideal.Quotient.mkₐ R₁ I) = (Ideal.Quotient.mkₐ R₁ J).comp f
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_3<VAR>CommRing A<VAR>I : Ideal A<VAR>Algebra R A<GOAL>Function.Injective ⇑(algebraMap (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I))
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I J : Ideal A<VAR>h : I = J<VAR>x : A<GOAL>(Ideal.quotientEquivAlgOfEq R₁ h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I J : Ideal A<VAR>h : I = J<GOAL>(Ideal.quotientEquivAlgOfEq R₁ h).symm = Ideal.quotientEquivAlgOfEq R₁ ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<GOAL>RingHom.ker (DoubleQuot.quotLeftToQuotSup I J) = Ideal.map (Ideal.Quotient.mk I) J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<GOAL>RingHom.ker (DoubleQuot.quotQuotMk I J) = I ⊔ J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivQuotSup I J) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk (I ⊔ J)) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivQuotSup I J).symm ((Ideal.Quotient.mk (I ⊔ J)) x) = (DoubleQuot.quotQuotMk I J) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivComm I J) ((DoubleQuot.quotQuotMk I J) x) = (DoubleQuot.quotQuotMk J I) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<GOAL>(↑(DoubleQuot.quotQuotEquivComm I J)).comp (DoubleQuot.quotQuotMk I J) = DoubleQuot.quotQuotMk J I
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<GOAL>(DoubleQuot.quotQuotEquivComm I J).symm = DoubleQuot.quotQuotEquivComm J I
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<VAR>h : I ≤ J<GOAL>(DoubleQuot.quotQuotEquivQuotOfLE h) ((DoubleQuot.quotQuotMk I J) x) = (Ideal.Quotient.mk J) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<VAR>h : I ≤ J<GOAL>(DoubleQuot.quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = (DoubleQuot.quotQuotMk I J) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>(↑(DoubleQuot.quotQuotEquivQuotOfLE h)).comp (DoubleQuot.quotQuotMk I J) = Ideal.Quotient.mk J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>(↑(DoubleQuot.quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = DoubleQuot.quotQuotMk I J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivComm I J) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) ((Ideal.Quotient.mk I) x)) = (algebraMap R ((R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivQuotSup I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R (A ⧸ I ⊔ J)) x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>x : R<GOAL>(DoubleQuot.quotQuotEquivComm I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) = (algebraMap R ((A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I)) x
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotLeftToQuotSupₐ R I J) = DoubleQuot.quotLeftToQuotSup I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotLeftToQuotSupₐ R I J) = ⇑(DoubleQuot.quotLeftToQuotSup I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotQuotToQuotSupₐ R I J) = DoubleQuot.quotQuotToQuotSup I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotQuotToQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotToQuotSup I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMk I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotQuotMkₐ R I J) = ⇑(DoubleQuot.quotQuotMk I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = DoubleQuot.liftSupQuotQuotMk I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = ⇑(DoubleQuot.liftSupQuotQuotMk I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = DoubleQuot.quotQuotEquivQuotSup I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J) = ⇑(DoubleQuot.quotQuotEquivQuotSup I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = (DoubleQuot.quotQuotEquivQuotSup I J).symm
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotQuotEquivQuotSupₐ R I J).symm = ⇑(DoubleQuot.quotQuotEquivQuotSup I J).symm
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>↑(DoubleQuot.quotQuotEquivCommₐ R I J) = DoubleQuot.quotQuotEquivComm I J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>⇑(DoubleQuot.quotQuotEquivCommₐ R I J) = ⇑(DoubleQuot.quotQuotEquivComm I J)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>(DoubleQuot.quotQuotEquivCommₐ R I J).symm = DoubleQuot.quotQuotEquivCommₐ R J I
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<GOAL>(↑(DoubleQuot.quotQuotEquivCommₐ R I J)).comp (DoubleQuot.quotQuotMkₐ R I J) = DoubleQuot.quotQuotMkₐ R J I
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = DoubleQuot.quotQuotEquivQuotOfLE h
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h)
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = (DoubleQuot.quotQuotEquivQuotOfLE h).symm
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h).symm
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>(↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)).comp (DoubleQuot.quotQuotMkₐ R I J) = Ideal.Quotient.mkₐ R J
<VAR>R : Type u<VAR>A : Type u_1<VAR>CommSemiring R<VAR>CommRing A<VAR>Algebra R A<VAR>I J : Ideal A<VAR>h : I ≤ J<GOAL>(↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm).comp (Ideal.Quotient.mkₐ R J) = DoubleQuot.quotQuotMkₐ R I J
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>self : P.IsRootPositive B<VAR>i : ι<VAR>x y : M<GOAL>(B ((P.reflection i) x)) ((P.reflection i) y) = (B x) y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>self : P.IsRootPositive B<VAR>i : ι<GOAL>0 < (B (P.root i)) (P.root i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>self : P.IsRootPositive B<VAR>x y : M<GOAL>(B x) y = (B y) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>2 * (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>0 < (B (P.root i)) (P.root j) ↔ 0 < P.pairing i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>0 < P.pairing i j ↔ 0 < P.pairing j i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>0 ≤ P.coxeterWeight i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>(B (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>P.pairing i j = 0 ↔ P.pairing j i = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>LinearOrderedCommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>P.IsRootPositive B<VAR>i j : ι<GOAL>P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Nontrivial M<GOAL>LinearMap.det 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Finite ι<VAR>b : Basis ι R M<GOAL>Module.Finite R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Ideal S<VAR>P.IsPrime<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔ ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r<GOAL>f.SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>h : Function.Surjective ⇑f<GOAL>f.SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>(algebraMap R S).SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>T : Type u_3<VAR>CommRing T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : g.SurjectiveOnStalks<VAR>hf : f.SurjectiveOnStalks<GOAL>(g.comp f).SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>T : Type u_3<VAR>CommRing T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : (g.comp f).SurjectiveOnStalks<GOAL>g.SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_3<VAR>CommRing T<VAR>Algebra R T<VAR>hf₂ : (algebraMap R T).SurjectiveOnStalks<VAR>x : TensorProduct R S T<VAR>J : Ideal T<VAR>hJ : J.IsPrime<GOAL>∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_3<VAR>CommRing T<VAR>Algebra R T<VAR>hf : (algebraMap R T).SurjectiveOnStalks<GOAL>(algebraMap S (TensorProduct R S T)).SurjectiveOnStalks
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>LocalRing S<VAR>IsLocalRingHom f<GOAL>f.SurjectiveOnStalks ↔ Function.Surjective ⇑f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : RootPairing ι R M N<VAR>i : ι<GOAL>(self.toLin (self.root i)) (self.coroot i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : RootPairing ι R M N<VAR>i j : ι<GOAL>self.root j - (self.toLin (self.root j)) (self.coroot i) • self.root i = self.root ((self.reflection_perm i) j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : RootPairing ι R M N<VAR>i j : ι<GOAL>self.coroot j - (self.toLin (self.root i)) (self.coroot j) • self.coroot i = self.coroot ((self.reflection_perm i) j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>self : RootSystem ι R M N<GOAL>Submodule.span R (Set.range ⇑self.root) = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>CharZero R<GOAL>P.root i ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>CharZero R<GOAL>P.coroot i ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<GOAL>P.flip.flip = P
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>(P.toLin (P.root i)) (P.coroot j) = P.pairing i j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>(P.toLin.flip (P.coroot i)) (P.root j) = P.pairing j i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>P.pairing i i = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>(P.toLin.flip (P.coroot i)) (P.root i) = 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.root ((P.reflection_perm i) j) = (P.reflection i) (P.root j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>Set.MapsTo (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>x : M<GOAL>(P.reflection i) x = x - (P.toLin x) (P.coroot i) • P.root i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>(P.reflection i) (P.root j) = P.root j - P.pairing j i • P.root i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>(P.reflection i) (P.root i) = -P.root i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<VAR>x : M<GOAL>(P.reflection i) ((P.reflection i) x) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>Set.BijOn (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>⇑(P.reflection i) '' Set.range ⇑P.root = Set.range ⇑P.root
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.coroot ((P.reflection_perm i) j) = (P.coreflection i) (P.coroot j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : RootPairing ι R M N<VAR>i : ι<GOAL>Set.MapsTo (⇑(P.coreflection i)) (Set.range ⇑P.coroot) (Set.range ⇑P.coroot)