ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>(LinearMap.range f).toAddSubmonoid = AddMonoidHom.mrange f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>x : M₂<GOAL>x ∈ LinearMap.range f ↔ ∃ y, f y = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<GOAL>LinearMap.range f = Submodule.map f ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>x : M<GOAL>f x ∈ LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.range LinearMap.id = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>RingHomSurjective τ₁₂<VAR>RingHomSurjective τ₂₃<VAR>RingHomSurjective τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.range (g.comp f) = Submodule.map g (LinearMap.range f)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>RingHomSurjective τ₂₃<VAR>RingHomSurjective τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.range (g.comp f) ≤ LinearMap.range g
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<GOAL>LinearMap.range f = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>p : Submodule R₂ M₂<GOAL>LinearMap.range f ≤ p ↔ Submodule.comap f p = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>p : Submodule R M<GOAL>Submodule.map f p ≤ LinearMap.range f
<VAR>R : Type u_12<VAR>R₂ : Type u_13<VAR>M : Type u_14<VAR>M₂ : Type u_15<VAR>Semiring R<VAR>Ring R₂<VAR>AddCommMonoid M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.range (-f) = LinearMap.range f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<GOAL>LinearMap.range (f.domRestrict S) ≤ LinearMap.range f
<VAR>M : Type u_12<VAR>M₂ : Type u_13<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>f : M →+ M₂<GOAL>LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>p : Submodule R₂ M₂<VAR>h : p ≤ LinearMap.range f<GOAL>Submodule.map f (Submodule.comap f p) = p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<GOAL>f.iterateRange n = LinearMap.range (f ^ n)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomSurjective τ₂₁<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[τ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<GOAL>LinearMap.range (LinearMap.codRestrict p f hf) = Submodule.comap p.subtype (LinearMap.range f)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>q : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.comap f q) = LinearMap.range f ⊓ q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>q : Submodule R₂ M₂<VAR>h : q ≤ LinearMap.range f<GOAL>Submodule.map f (Submodule.comap f q) = q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<GOAL>LinearMap.range 0 = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.range f ≤ ⊥ ↔ f = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.range f = ⊥ ↔ f = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.range f ≤ LinearMap.ker g ↔ g.comp f = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>hf : LinearMap.range f = ⊤<VAR>p p' : Submodule R₂ M₂<GOAL>Submodule.comap f p ≤ Submodule.comap f p' ↔ p ≤ p'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>hf : LinearMap.range f = ⊤<GOAL>Function.Injective (Submodule.comap f)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>(LinearMap.range f).toAddSubgroup = f.toAddMonoidHom.range
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>RingHomSurjective τ₁₂<VAR>p : Submodule R M<GOAL>LinearMap.ker f ≤ p ↔ ∃ y ∈ LinearMap.range f, ⇑f ⁻¹' {y} ⊆ ↑p
<VAR>K : Type u_4<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<VAR>h : a ≠ 0<GOAL>LinearMap.range (a • f) = LinearMap.range f
<VAR>K : Type u_4<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<GOAL>LinearMap.range (a • f) = ⨆ (_ : a ≠ 0), LinearMap.range f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<GOAL>Submodule.map f ⊤ = LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>LinearMap.range p.subtype = p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>p' : Submodule R ↥p<GOAL>Submodule.map p.subtype p' ≤ p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.map p.subtype ⊤ = p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Submodule.comap p.subtype p' = ⊤ ↔ p ≤ p'
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.comap p.subtype p = ⊤
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>h : p ≤ q<GOAL>LinearMap.range (Submodule.inclusion h) = Submodule.comap q.subtype p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<GOAL>Submodule.map p'.subtype (LinearMap.range (Submodule.inclusion h)) = p
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>p' : Submodule R ↥p<GOAL>(Submodule.MapSubtype.orderEmbedding p) p' = Submodule.map p.subtype p'
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>q : Submodule R ↥p<GOAL>↑(p.mapIic q) = Submodule.map p.subtype q
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : ↥(LinearMap.ker f) →ₗ[R] M), f.comp u = f.comp v → u = v<GOAL>LinearMap.ker f = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>RingHomSurjective τ₁₂<VAR>RingHomSurjective τ₂₃<VAR>RingHomSurjective τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>hf : LinearMap.range f = ⊤<GOAL>LinearMap.range (g.comp f) = LinearMap.range g
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_11<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>x : M'<GOAL>x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_11<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>hNO : N ≤ O<VAR>x : M'<GOAL>x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yN : y ∈ N), ϕ ⟨y, ⋯⟩ = x
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_11<VAR>AddCommGroup M'<VAR>Module R M'<VAR>O : Submodule R M<VAR>ϕ : ↥O →ₗ[R] M'<VAR>N : Submodule R M<VAR>hNO : N ≤ O<GOAL>ϕ.submoduleImage N = LinearMap.range (ϕ ∘ₗ Submodule.inclusion hNO)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.range f.rangeRestrict = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.ker f.rangeRestrict = LinearMap.ker f
<VAR>k : Type u_1<VAR>CommSemiring k<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra k A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module k M<VAR>Module A M<VAR>IsScalarTower k A M<VAR>N : Type u_4<VAR>AddCommMonoid N<VAR>Module k N<VAR>Module A N<VAR>IsScalarTower k A N<VAR>fₗ : M →ₗ[A] N<GOAL>(LinearMap.restrictScalarsLinearMap k A M N) fₗ = ↑k fₗ
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>y : M<GOAL>y ∈ LinearMap.ker f ↔ f y = 0
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.ker LinearMap.id = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>x : ↥(LinearMap.ker f)<GOAL>f ↑x = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>(LinearMap.ker f).toAddSubmonoid = AddMonoidHom.mker f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>f.comp (LinearMap.ker f).subtype = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.ker (g.comp f) = Submodule.comap f (LinearMap.ker g)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.ker f ≤ LinearMap.ker (g.comp f)
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<GOAL>LinearMap.ker f ⊔ LinearMap.ker g ≤ LinearMap.ker (f ∘ₗ g)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>p : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.ker f ≤ Submodule.comap f p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>LinearMap.ker f = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₁] M<VAR>h : g.comp f = LinearMap.id<GOAL>LinearMap.ker f = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<VAR>p : Submodule R M<GOAL>p ≤ LinearMap.ker f ↔ Submodule.map f p = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₂₁ : R₂ →+* R<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[τ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<GOAL>LinearMap.ker (LinearMap.codRestrict p f hf) = LinearMap.ker f
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>f : M →ₗ[R] M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<GOAL>LinearMap.ker (f.restrict hf) = LinearMap.ker (f.domRestrict p)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<GOAL>LinearMap.ker 0 = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.ker f = ⊤ ↔ f = 0
<VAR>M : Type u_13<VAR>M₂ : Type u_14<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>f : M →+ M₂<GOAL>LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>LinearMap.ker f = ⊥
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>n : ℕ<GOAL>f.iterateKer n = LinearMap.ker (f ^ n)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>(LinearMap.ker f).toAddSubgroup = f.toAddMonoidHom.ker
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>x y : M<GOAL>x - y ∈ LinearMap.ker f ↔ f x = f y
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>s : Set M<VAR>h : s ⊆ ↑p<VAR>hd : Disjoint p (LinearMap.ker f)<GOAL>Set.InjOn (⇑f) s
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>LinearMap.ker f = ⊥ ↔ Function.Injective ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>LinearMap.ker f = ⊥ ↔ Function.Injective ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Ring R<VAR>Ring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<GOAL>Function.Injective ⇑(f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>hf : ∀ x ∈ p, f x ∈ p<GOAL>Function.Injective ⇑(f.restrict hf) ↔ Disjoint p (LinearMap.ker f)
<VAR>K : Type u_5<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<VAR>h : a ≠ 0<GOAL>LinearMap.ker (a • f) = LinearMap.ker f
<VAR>K : Type u_5<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>a : K<GOAL>LinearMap.ker (a • f) = ⨅ (_ : a ≠ 0), LinearMap.ker f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>Submodule.comap f ⊥ = LinearMap.ker f
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>LinearMap.ker p.subtype = ⊥
<VAR>R : Type u_1<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<GOAL>LinearMap.ker (Submodule.inclusion h) = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>hg : LinearMap.ker g = ⊥<GOAL>LinearMap.ker (g.comp f) = LinearMap.ker f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_6<VAR>M₂ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃ₛₗ[σ₁₂] M₂<GOAL>LinearMap.ker ↑e = ⊥