ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed k<VAR>Algebra k K<VAR>Algebra.IsSeparable k K<GOAL>Function.Surjective ⇑(algebraMap k K)
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed k<VAR>Algebra k K<VAR>L : IntermediateField k K<VAR>Algebra.IsSeparable k ↥L<GOAL>L = ⊥
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>Algebra k K<VAR>self : IsSepClosure k K<GOAL>IsSepClosed K
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>Algebra k K<VAR>self : IsSepClosure k K<GOAL>Algebra.IsSeparable k K
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>Algebra k K<GOAL>IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Field M<VAR>Algebra K M<VAR>IsSepClosed M<VAR>E : Type u_1<VAR>Field E<VAR>Algebra K E<VAR>Algebra L E<VAR>IsScalarTower K L E<VAR>Algebra.IsSeparable L E<GOAL>Function.Surjective fun φ => φ.comp (IsScalarTower.toAlgHom K L E)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Field M<VAR>Algebra K M<VAR>IsSepClosed M<VAR>Algebra.IsSeparable K L<GOAL>IsSepClosed.lift = Classical.choice ⋯
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>(minpoly A x).Monic
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial A<VAR>hx : IsIntegral A x<GOAL>minpoly A x ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>hx : ¬IsIntegral A x<GOAL>minpoly A x = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>CommRing A<VAR>Ring B<VAR>Ring B'<VAR>Algebra A B<VAR>Algebra A B'<VAR>f : B →ₐ[A] B'<VAR>hf : Function.Injective ⇑f<VAR>x : B<GOAL>minpoly A (f x) = minpoly A x
<VAR>A : Type u_1<VAR>B' : Type u_3<VAR>CommRing A<VAR>Ring B'<VAR>Algebra A B'<VAR>B : Type u_4<VAR>CommRing B<VAR>Algebra A B<VAR>Algebra B B'<VAR>IsScalarTower A B B'<VAR>h : Function.Injective ⇑(algebraMap B B')<VAR>x : B<GOAL>minpoly A ((algebraMap B B') x) = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>CommRing A<VAR>Ring B<VAR>Ring B'<VAR>Algebra A B<VAR>Algebra A B'<VAR>f : B ≃ₐ[A] B'<VAR>x : B<GOAL>minpoly A (f x) = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<GOAL>(Polynomial.aeval x) (minpoly A x) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>CommRing A<VAR>Ring B<VAR>Ring B'<VAR>Algebra A B<VAR>Algebra A B'<VAR>f : B →ₐ[A] B'<VAR>x : B<GOAL>(Polynomial.aeval (f x)) (minpoly A x) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<GOAL>minpoly A x ≠ 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>R : Type u_4<VAR>Semiring R<VAR>Nontrivial R<VAR>f : A →+* R<GOAL>Polynomial.map f (minpoly A x) ≠ 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<GOAL>¬IsUnit (minpoly A x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>hx : (minpoly A x).degree = 1<GOAL>x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>pmonic : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<GOAL>(minpoly A x).degree ≤ p.degree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hm : p.Monic<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hl : ∀ (q : A[X]), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0<GOAL>p = minpoly A x
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Subsingleton B<GOAL>minpoly A x = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>hx : IsIntegral A x<GOAL>0 < (minpoly A x).natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>hx : IsIntegral A x<GOAL>0 < (minpoly A x).degree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<GOAL>(minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<GOAL>(minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>Nontrivial B<VAR>int : IsIntegral A x<GOAL>2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range
<VAR>A : Type u_1<VAR>CommRing A<VAR>B : Type u_4<VAR>CommRing B<VAR>Algebra A B<VAR>Nontrivial B<VAR>S : Subalgebra A B<VAR>x : B<VAR>int : IsIntegral (↥S) x<GOAL>2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>a : A<VAR>hf : Function.Injective ⇑(algebraMap A B)<GOAL>minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>a : A[X]<VAR>hx : IsIntegral A x<VAR>hamonic : a.Monic<VAR>hdvd : DvdNotUnit a (minpoly A x)<GOAL>(Polynomial.aeval x) a ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>Ring B<VAR>Algebra A B<VAR>x : B<VAR>IsDomain A<VAR>IsDomain B<VAR>hx : IsIntegral A x<GOAL>Irreducible (minpoly A x)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥f.domain<GOAL>f.toFun x = ↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : f.domain = g.domain<VAR>h' : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y<GOAL>f = g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>↑f 0 = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<GOAL>f = g ↔ ∃ (_ : f.domain = g.domain), ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>s : Submodule R E<VAR>f g : ↥s →ₗ[R] F<VAR>h : f = g<GOAL>{ domain := s, toFun := f } = { domain := s, toFun := g }
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x y : ↥f.domain<GOAL>↑f (x + y) = ↑f x + ↑f y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥f.domain<GOAL>↑f (-x) = -↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x y : ↥f.domain<GOAL>↑f (x - y) = ↑f x - ↑f y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>c : R<VAR>x : ↥f.domain<GOAL>↑f (c • x) = c • ↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p : Submodule R E<VAR>f : ↥p →ₗ[R] F<VAR>x : ↥p<GOAL>↑{ domain := p, toFun := f } x = f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<GOAL>(LinearPMap.mkSpanSingleton' x y H).domain = Submodule.span R {x}
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>c : R<VAR>h : c • x ∈ (LinearPMap.mkSpanSingleton' x y H).domain<GOAL>↑(LinearPMap.mkSpanSingleton' x y H) ⟨c • x, h⟩ = c • y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>h : x ∈ (LinearPMap.mkSpanSingleton' x y H).domain<GOAL>↑(LinearPMap.mkSpanSingleton' x y H) ⟨x, h⟩ = y
<VAR>K : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>DivisionRing K<VAR>AddCommGroup E<VAR>Module K E<VAR>AddCommGroup F<VAR>Module K F<VAR>x : E<VAR>hx : x ≠ 0<VAR>y : F<GOAL>↑(LinearPMap.mkSpanSingleton x y hx) ⟨x, ⋯⟩ = y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p : Submodule R E<VAR>p' : Submodule R F<VAR>x : ↥(p.prod p')<GOAL>↑(LinearPMap.fst p p') x = (↑x).1
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>p : Submodule R E<VAR>p' : Submodule R F<VAR>x : ↥(p.prod p')<GOAL>↑(LinearPMap.snd p p') x = (↑x).2
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>T S : E →ₗ.[R] F<VAR>h : T ≤ S<VAR>x : ↥T.domain<GOAL>↑T x = ↑S ((Submodule.inclusion ⋯) x)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>T S : E →ₗ.[R] F<VAR>h : T ≤ S<VAR>x : ↥T.domain<GOAL>∃ y, ↑x = ↑y ∧ ↑T x = ↑S y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>hle : f ≤ g<VAR>heq : f.domain = g.domain<GOAL>f = g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>H : f.domain ≤ f.eqLocus g<GOAL>f ≤ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<GOAL>StrictMono LinearPMap.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>(f.sup g h).domain = f.domain ⊔ g.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>z : ↥(f.domain ⊔ g.domain)<VAR>hz : ↑x + ↑y = ↑z<GOAL>↑(f.sup g H) z = ↑f x + ↑g y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>f ≤ f.sup g h
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>g ≤ f.sup g h
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g h : E →ₗ.[R] F<VAR>H : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>fh : f ≤ h<VAR>gh : g ≤ h<GOAL>f.sup g H ≤ h
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : Disjoint f.domain g.domain<VAR>x : ↥f.domain<VAR>y : ↥g.domain<VAR>hxy : ↑x = ↑y<GOAL>↑f x = ↑g y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<GOAL>LinearPMap.domain 0 = ⊤
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>x : ↥⊤<GOAL>↑0 x = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>M : Type u_5<VAR>Monoid M<VAR>DistribMulAction M F<VAR>SMulCommClass R M F<VAR>a : M<VAR>f : E →ₗ.[R] F<GOAL>(a • f).domain = f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>M : Type u_5<VAR>Monoid M<VAR>DistribMulAction M F<VAR>SMulCommClass R M F<VAR>a : M<VAR>f : E →ₗ.[R] F<VAR>x : ↥(a • f).domain<GOAL>↑(a • f) x = a • ↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>M : Type u_5<VAR>Monoid M<VAR>DistribMulAction M F<VAR>SMulCommClass R M F<VAR>a : M<VAR>f : E →ₗ.[R] F<GOAL>↑(a • f) = a • ↑f
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>(-f).domain = f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥(-f).domain<GOAL>↑(-f) x = -↑f x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<GOAL>(f + g).domain = f.domain ⊓ g.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>x : ↥(f.domain ⊓ g.domain)<GOAL>↑(f + g) x = ↑f ⟨↑x, ⋯⟩ + ↑g ⟨↑x, ⋯⟩
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ[R] F<VAR>g : E →ₗ.[R] F<GOAL>(f +ᵥ g).domain = g.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ[R] F<VAR>g : E →ₗ.[R] F<VAR>x : ↥(f +ᵥ g).domain<GOAL>↑(f +ᵥ g) x = f ↑x + ↑g x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ[R] F<VAR>g : E →ₗ.[R] F<GOAL>↑(f +ᵥ g) = ⇑(f ∘ₗ g.domain.subtype) + ↑g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<GOAL>(f - g).domain = f.domain ⊓ g.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>x : ↥(f.domain ⊓ g.domain)<GOAL>↑(f - g) x = ↑f ⟨↑x, ⋯⟩ - ↑g ⟨↑x, ⋯⟩
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>K : Type u_5<VAR>DivisionRing K<VAR>Module K E<VAR>Module K F<VAR>f : E →ₗ.[K] F<VAR>x : E<VAR>y : F<VAR>hx : x ∉ f.domain<GOAL>(f.supSpanSingleton x y hx).domain = f.domain ⊔ Submodule.span K {x}
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>K : Type u_5<VAR>DivisionRing K<VAR>Module K E<VAR>Module K F<VAR>f : E →ₗ.[K] F<VAR>x : E<VAR>y : F<VAR>hx : x ∉ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>c : K<GOAL>↑(f.supSpanSingleton x y hx) ⟨x' + c • x, ⋯⟩ = ↑f ⟨x', hx'⟩ + c • y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<GOAL>∃ f, { domain := sSup (LinearPMap.domain '' c), toFun := f } ∈ upperBounds c
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>f : E →ₗ.[R] F<VAR>hf : f ∈ c<GOAL>f ≤ LinearPMap.sSup c hc
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>g : E →ₗ.[R] F<VAR>hg : ∀ f ∈ c, f ≤ g<GOAL>LinearPMap.sSup c hc ≤ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>c : Set (E →ₗ.[R] F)<VAR>hc : DirectedOn (fun x x_1 => x ≤ x_1) c<VAR>l : E →ₗ.[R] F<VAR>hl : l ∈ c<VAR>x : ↥l.domain<GOAL>↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ[R] F<VAR>p : Submodule R E<VAR>x : ↥p<GOAL>↑(f.toPMap p) x = f ↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ[R] F<VAR>p : Submodule R E<GOAL>(f.toPMap p).domain = p
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>Module R G<VAR>g : F →ₗ[R] G<VAR>f : E →ₗ.[R] F<VAR>x : ↥(g.compPMap f).domain<GOAL>↑(g.compPMap f) x = g (↑f x)
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>G : Type u_4<VAR>AddCommGroup G<VAR>Module R G<VAR>f : E →ₗ.[R] G<VAR>g : F →ₗ.[R] G<VAR>x : ↥(f.coprod g).domain<GOAL>↑(f.coprod g) x = ↑f ⟨(↑x).1, ⋯⟩ + ↑g ⟨(↑x).2, ⋯⟩
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<GOAL>(f.domRestrict S).domain = S ⊓ f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<VAR>x : ↥(S ⊓ f.domain)<VAR>y : ↥f.domain<VAR>h : ↑x = ↑y<GOAL>↑(f.domRestrict S) x = ↑f y
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>S : Submodule R E<GOAL>f.domRestrict S ≤ f
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E × F<GOAL>x ∈ f.graph ↔ ∃ y, (↑y, ↑f y) = x
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E × F<GOAL>x ∈ f.graph ↔ ∃ y, ↑y = x.1 ∧ ↑f y = x.2
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥f.domain<GOAL>(↑x, ↑f x) ∈ f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>Submodule.map (LinearMap.fst R E F) f.graph = f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>Submodule.map (LinearMap.snd R E F) f.graph = LinearMap.range f.toFun
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>M : Type u_5<VAR>Monoid M<VAR>DistribMulAction M F<VAR>SMulCommClass R M F<VAR>f : E →ₗ.[R] F<VAR>z : M<GOAL>(z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<GOAL>(-f).graph = Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x y : E<VAR>x' y' : F<VAR>hx : (x, x') ∈ f.graph<VAR>hy : (y, y') ∈ f.graph<VAR>hxy : x = y<GOAL>x' = y'
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x y : E × F<VAR>hx : x ∈ f.graph<VAR>hy : y ∈ f.graph<VAR>hxy : x.1 = y.1<GOAL>x.2 = y.2
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>x' : F<VAR>h : (x, x') ∈ f.graph<VAR>hx : x = 0<GOAL>x' = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E<GOAL>x ∈ f.domain ↔ ∃ y, (x, y) ∈ f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>h : (x, y) ∈ f.graph<GOAL>x ∈ f.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ f.domain<GOAL>y = ↑f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f : E →ₗ.[R] F<VAR>y : F<GOAL>y ∈ Set.range ↑f ↔ ∃ x, (x, y) ∈ f.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph = g.graph<VAR>x : E<GOAL>x ∈ f.domain ↔ x ∈ g.domain
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph ≤ g.graph<GOAL>f ≤ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : f ≤ g<GOAL>f.graph ≤ g.graph
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<GOAL>f.graph ≤ g.graph ↔ f ≤ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>f g : E →ₗ.[R] F<VAR>h : f.graph = g.graph<GOAL>f = g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ Submodule.map (LinearMap.fst R E F) g<GOAL>∃! b, (a, b) ∈ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ Submodule.map (LinearMap.fst R E F) g<GOAL>(a, Submodule.valFromGraph hg ha) ∈ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<GOAL>g.toLinearPMap.domain = Submodule.map (LinearMap.fst R E F) g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : ↥(Submodule.map (LinearMap.fst R E F) g)<GOAL>↑g.toLinearPMap x = Submodule.valFromGraph hg ⋯
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<VAR>x : ↥(Submodule.map (LinearMap.fst R E F) g)<GOAL>(↑x, ↑g.toLinearPMap x) ∈ g
<VAR>R : Type u_1<VAR>Ring R<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module R E<VAR>F : Type u_3<VAR>AddCommGroup F<VAR>Module R F<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<GOAL>g.toLinearPMap.graph = g