ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>m : M<GOAL>((CliffordAlgebra.foldr Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>r : R<GOAL>((CliffordAlgebra.foldr Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((CliffordAlgebra.foldr Q f hf) n) 1 = n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>a b : CliffordAlgebra Q<GOAL>((CliffordAlgebra.foldr Q f hf) n) (a * b) = ((CliffordAlgebra.foldr Q f hf) (((CliffordAlgebra.foldr Q f hf) n) b)) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>l : List M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((CliffordAlgebra.foldr Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = List.foldr (fun m n => (f m) n) n l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>x : CliffordAlgebra Q<GOAL>((CliffordAlgebra.foldl Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldr Q f hf) n) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>x : CliffordAlgebra Q<GOAL>((CliffordAlgebra.foldr Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldl Q f hf) n) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>m : M<GOAL>((CliffordAlgebra.foldl Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>r : R<GOAL>((CliffordAlgebra.foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((CliffordAlgebra.foldl Q f hf) n) 1 = n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<VAR>a b : CliffordAlgebra Q<GOAL>((CliffordAlgebra.foldl Q f hf) n) (a * b) = ((CliffordAlgebra.foldl Q f hf) (((CliffordAlgebra.foldl Q f hf) n) a)) b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>l : List M<VAR>f : M →ₗ[R] N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x<VAR>n : N<GOAL>((CliffordAlgebra.foldl Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod = List.foldl (fun m n => (f n) m) n l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (CliffordAlgebra.ι Q) m)<VAR>x : CliffordAlgebra Q<GOAL>P x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((CliffordAlgebra.ι Q) m * x)<VAR>x : CliffordAlgebra Q<GOAL>P x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>m : M<VAR>x_fx : CliffordAlgebra Q × N<GOAL>((CliffordAlgebra.foldr'Aux Q f) m) x_fx = ((CliffordAlgebra.ι Q) m * x_fx.1, (f m) x_fx)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>v : M<VAR>x_fx : CliffordAlgebra Q × N<GOAL>((CliffordAlgebra.foldr'Aux Q f) v) (((CliffordAlgebra.foldr'Aux Q f) v) x_fx) = Q v • x_fx
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>r : R<GOAL>(CliffordAlgebra.foldr' Q f hf n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<GOAL>(CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m) = (f m) (1, n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Q : QuadraticForm R M<VAR>f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N<VAR>hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx<VAR>n : N<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m * x) = (f m) (x, (CliffordAlgebra.foldr' Q f hf n) x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M → N → P<VAR>H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n<VAR>H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = ρ₁₂ c • f m n<VAR>H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂<VAR>H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = σ₁₂ c • f m n<VAR>m : M<VAR>n : N<GOAL>((LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Pₗ : Type u_12<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module S N<VAR>Module R Pₗ<VAR>Module S Pₗ<VAR>SMulCommClass S R Pₗ<VAR>f : M → N → Pₗ<VAR>H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n<VAR>H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = c • f m n<VAR>H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂<VAR>H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = c • f m n<VAR>m : M<VAR>n : N<GOAL>((LinearMap.mk₂' R S f H1 H2 H3 H4) m) n = f m n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>H : ∀ (m : M) (n : N), (f m) n = (g m) n<GOAL>f = g
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>h : f = g<VAR>x : M<VAR>y : N<GOAL>(f x) y = (g x) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<GOAL>f = g ↔ ∀ (m : M) (n : N), (f m) n = (g m) n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>m : M<VAR>n : N<GOAL>(f.flip n) m = (f m) n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<GOAL>f.flip.flip = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>H : f.flip = g.flip<GOAL>f = g
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>y : N<GOAL>(f 0) y = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>N : Type u_6<VAR>M' : Type u_13<VAR>P' : Type u_15<VAR>AddCommMonoid N<VAR>AddCommGroup M'<VAR>AddCommGroup P'<VAR>Module S N<VAR>Module R M'<VAR>Module R₂ P'<VAR>Module S₂ P'<VAR>SMulCommClass S₂ R₂ P'<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P'<VAR>x : M'<VAR>y : N<GOAL>(f (-x)) y = -(f x) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>N : Type u_6<VAR>M' : Type u_13<VAR>P' : Type u_15<VAR>AddCommMonoid N<VAR>AddCommGroup M'<VAR>AddCommGroup P'<VAR>Module S N<VAR>Module R M'<VAR>Module R₂ P'<VAR>Module S₂ P'<VAR>SMulCommClass S₂ R₂ P'<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P'<VAR>x y : M'<VAR>z : N<GOAL>(f (x - y)) z = (f x) z - (f y) z
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>x₁ x₂ : M<VAR>y : N<GOAL>(f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M₂ : Type u_8<VAR>N₂ : Type u_9<VAR>P₂ : Type u_10<VAR>AddCommMonoid M₂<VAR>AddCommMonoid N₂<VAR>AddCommMonoid P₂<VAR>Module R M₂<VAR>Module S N₂<VAR>Module R P₂<VAR>Module S₂ P₂<VAR>SMulCommClass S₂ R P₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂<VAR>r : R<VAR>x : M₂<VAR>y : N₂<GOAL>(f (r • x)) y = r • (f x) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>r : R<VAR>x : M<VAR>y : N<GOAL>(f (r • x)) y = ρ₁₂ r • (f x) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>ι : Type u_16<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>t : Finset ι<VAR>x : ι → M<VAR>y : N<GOAL>(f (∑ i ∈ t, x i)) y = ∑ i ∈ t, (f (x i)) y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>q : Submodule S N<VAR>x : M<VAR>y : ↥q<GOAL>((f.domRestrict₂ q) x) y = (f x) ↑y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>R₂ : Type u_3<VAR>Semiring R₂<VAR>S₂ : Type u_4<VAR>Semiring S₂<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>p : Submodule R M<VAR>q : Submodule S N<VAR>x : ↥p<VAR>y : ↥q<GOAL>((f.domRestrict₁₂ p q) x) y = (f ↑x) ↑y
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Pₗ : Type u_12<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module S N<VAR>Module R Pₗ<VAR>Module S Pₗ<VAR>SMulCommClass S R Pₗ<VAR>R' : Type u_16<VAR>S' : Type u_17<VAR>Semiring R'<VAR>Semiring S'<VAR>Module R' M<VAR>Module S' N<VAR>Module R' Pₗ<VAR>Module S' Pₗ<VAR>SMulCommClass S' R' Pₗ<VAR>SMul S' S<VAR>IsScalarTower S' S N<VAR>IsScalarTower S' S Pₗ<VAR>SMul R' R<VAR>IsScalarTower R' R M<VAR>IsScalarTower R' R Pₗ<VAR>B : M →ₗ[R] N →ₗ[S] Pₗ<VAR>m : M<GOAL>∀ (x : N), ((LinearMap.restrictScalars₁₂ R' S' B) m) x = (B m) x
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Pₗ : Type u_12<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module S N<VAR>Module R Pₗ<VAR>Module S Pₗ<VAR>SMulCommClass S R Pₗ<VAR>R' : Type u_16<VAR>S' : Type u_17<VAR>Semiring R'<VAR>Semiring S'<VAR>Module R' M<VAR>Module S' N<VAR>Module R' Pₗ<VAR>Module S' Pₗ<VAR>SMulCommClass S' R' Pₗ<VAR>SMul S' S<VAR>IsScalarTower S' S N<VAR>IsScalarTower S' S Pₗ<VAR>SMul R' R<VAR>IsScalarTower R' R M<VAR>IsScalarTower R' R Pₗ<GOAL>Function.Injective (LinearMap.restrictScalars₁₂ R' S')
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>M : Type u_5<VAR>N : Type u_6<VAR>Pₗ : Type u_12<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module S N<VAR>Module R Pₗ<VAR>Module S Pₗ<VAR>SMulCommClass S R Pₗ<VAR>R' : Type u_16<VAR>S' : Type u_17<VAR>Semiring R'<VAR>Semiring S'<VAR>Module R' M<VAR>Module S' N<VAR>Module R' Pₗ<VAR>Module S' Pₗ<VAR>SMulCommClass S' R' Pₗ<VAR>SMul S' S<VAR>IsScalarTower S' S N<VAR>IsScalarTower S' S Pₗ<VAR>SMul R' R<VAR>IsScalarTower R' R M<VAR>IsScalarTower R' R Pₗ<VAR>B B' : M →ₗ[R] N →ₗ[S] Pₗ<GOAL>LinearMap.restrictScalars₁₂ R' S' B = LinearMap.restrictScalars₁₂ R' S' B' ↔ B = B'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : M → Nₗ → Pₗ<VAR>H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n<VAR>H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n<VAR>H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂<VAR>H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n<VAR>m : M<VAR>n : Nₗ<GOAL>((LinearMap.mk₂ R f H1 H2 H3 H4) m) n = f m n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R₂ : Type u_2<VAR>CommSemiring R₂<VAR>R₃ : Type u_3<VAR>CommSemiring R₃<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R₂ N<VAR>Module R₃ P<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P<VAR>m : M<VAR>n : N<GOAL>((LinearMap.lflip f) n) m = (f m) n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : M →ₗ[R] Nₗ<VAR>g : Nₗ →ₗ[R] Pₗ<VAR>x : M<GOAL>((LinearMap.lcomp R Pₗ f) g) x = g (f x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : M →ₗ[R] Nₗ<VAR>g : Nₗ →ₗ[R] Pₗ<GOAL>(LinearMap.lcomp R Pₗ f) g = g ∘ₗ f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R₂ : Type u_2<VAR>CommSemiring R₂<VAR>R₃ : Type u_3<VAR>CommSemiring R₃<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R₂ N<VAR>Module R₃ P<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] N<VAR>g : N →ₛₗ[σ₂₃] P<VAR>x : M<GOAL>((LinearMap.lcompₛₗ P σ₂₃ f) g) x = g (f x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : Nₗ →ₗ[R] Pₗ<VAR>g : M →ₗ[R] Nₗ<VAR>x : M<GOAL>(((LinearMap.llcomp R M Nₗ Pₗ) f) g) x = f (g x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : Nₗ →ₗ[R] Pₗ<VAR>g : M →ₗ[R] Nₗ<GOAL>((LinearMap.llcomp R M Nₗ Pₗ) f) g = f ∘ₗ g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R₂ : Type u_2<VAR>CommSemiring R₂<VAR>R₃ : Type u_3<VAR>CommSemiring R₃<VAR>R₄ : Type u_4<VAR>CommSemiring R₄<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Q : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R₂ N<VAR>Module R₃ P<VAR>Module R₄ Q<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₄₃ : R₄ →+* R₃<VAR>RingHomCompTriple σ₄₂ σ₂₃ σ₄₃<VAR>f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P<VAR>g : Q →ₛₗ[σ₄₂] N<VAR>m : M<VAR>q : Q<GOAL>((f.compl₂ g) m) q = (f m) (g q)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>R₂ : Type u_2<VAR>CommSemiring R₂<VAR>R₃ : Type u_3<VAR>CommSemiring R₃<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R₂ N<VAR>Module R₃ P<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P<GOAL>f.compl₂ LinearMap.id = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Mₗ : Type u_9<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>Qₗ : Type u_12<VAR>Qₗ' : Type u_13<VAR>AddCommMonoid Mₗ<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>AddCommMonoid Qₗ<VAR>AddCommMonoid Qₗ'<VAR>Module R Mₗ<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>Module R Qₗ<VAR>Module R Qₗ'<VAR>f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ<VAR>g : Qₗ →ₗ[R] Mₗ<VAR>g' : Qₗ' →ₗ[R] Nₗ<VAR>x : Qₗ<VAR>y : Qₗ'<GOAL>((f.compl₁₂ g g') x) y = (f (g x)) (g' y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Mₗ : Type u_9<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>AddCommMonoid Mₗ<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>Module R Mₗ<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ<GOAL>f.compl₁₂ LinearMap.id LinearMap.id = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Mₗ : Type u_9<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>Qₗ : Type u_12<VAR>Qₗ' : Type u_13<VAR>AddCommMonoid Mₗ<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>AddCommMonoid Qₗ<VAR>AddCommMonoid Qₗ'<VAR>Module R Mₗ<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>Module R Qₗ<VAR>Module R Qₗ'<VAR>f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ<VAR>g : Qₗ →ₗ[R] Mₗ<VAR>g' : Qₗ' →ₗ[R] Nₗ<VAR>hₗ : Function.Surjective ⇑g<VAR>hᵣ : Function.Surjective ⇑g'<GOAL>f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>Qₗ : Type u_12<VAR>AddCommMonoid M<VAR>AddCommMonoid Nₗ<VAR>AddCommMonoid Pₗ<VAR>AddCommMonoid Qₗ<VAR>Module R M<VAR>Module R Nₗ<VAR>Module R Pₗ<VAR>Module R Qₗ<VAR>f : M →ₗ[R] Nₗ →ₗ[R] Pₗ<VAR>g : Pₗ →ₗ[R] Qₗ<VAR>m : M<VAR>n : Nₗ<GOAL>((f.compr₂ g) m) n = g ((f m) n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<GOAL>(LinearMap.lsmul R M) r = DistribMulAction.toLinearMap R M r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>m : M<GOAL>((LinearMap.lsmul R M) r) m = r • m
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : R<VAR>hx : x ≠ 0<GOAL>Function.Injective ⇑((LinearMap.lsmul R M) x)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>a : R<VAR>ha : a ≠ 0<GOAL>LinearMap.ker ((LinearMap.lsmul R M) a) = ⊥
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<GOAL>(LinearMap.traceAux R b) f = ((LinearMap.toMatrix b b) f).trace
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>κ : Type u_1<VAR>DecidableEq κ<VAR>Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<GOAL>LinearMap.traceAux R b = LinearMap.traceAux R c
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } R M<VAR>f : M →ₗ[R] M<GOAL>(LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<GOAL>(LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
<VAR>R : Type u<VAR>CommSemiring R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] M<GOAL>(LinearMap.trace R M) (f * g) = (LinearMap.trace R M) (g * f)