ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>ι₃ : Type u_4<VAR>ι₄ : Type u_5<VAR>CommSemiring R<VAR>N₁ : Type u_6<VAR>AddCommMonoid N₁<VAR>Module R N₁<VAR>N₂ : Type u_7<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N : Type u_8<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>σa : ι₁ ≃ ι₃<VAR>σb : ι₂ ≃ ι₄<GOAL>MultilinearMap.domDomCongr (σa.sumCongr σb) (a.domCoprod b) = (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>M : Fin n → Type u_3<VAR>M₂ : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>(i : Fin n) → AddCommMonoid (M i)<VAR>(i : Fin n) → Module R (M i)<VAR>Module R M₂<VAR>f g : MultilinearMap R M M₂<VAR>ι₁ : Fin n → Type u_6<VAR>e : (i : Fin n) → Basis (ι₁ i) R (M i)<VAR>h : ∀ (v : (i : Fin n) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)<GOAL>f = g
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>Finite ι<VAR>f g : MultilinearMap R (fun x => M₂) M₃<VAR>ι₁ : Type u_6<VAR>e : Basis ι₁ R M₂<VAR>h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)<GOAL>f = g
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>a : M<GOAL>∀ (a_1 : CliffordAlgebra Q × CliffordAlgebra Q), ((CliffordAlgebra.contractLeftAux Q d) a) a_1 = d a • a_1.1 - (CliffordAlgebra.ι Q) a * a_1.2
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>v : M<VAR>x fx : CliffordAlgebra Q<GOAL>((CliffordAlgebra.contractLeftAux Q d) v) ((CliffordAlgebra.ι Q) v * x, ((CliffordAlgebra.contractLeftAux Q d) v) (x, fx)) = Q v • fx
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractRight x) d = CliffordAlgebra.reverse ((CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>a : M<VAR>b : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) a * b) = d a • b - (CliffordAlgebra.ι Q) a * (CliffordAlgebra.contractLeft d) b
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>a : M<VAR>b : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractRight (b * (CliffordAlgebra.ι Q) a)) d = d a • b - (CliffordAlgebra.contractRight b) d * (CliffordAlgebra.ι Q) a
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>r : R<VAR>b : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) = (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractLeft d) b
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>a : CliffordAlgebra Q<VAR>r : R<GOAL>(CliffordAlgebra.contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) = (CliffordAlgebra.contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>r : R<VAR>b : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d = (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractRight b) d
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>a : CliffordAlgebra Q<VAR>r : R<GOAL>(CliffordAlgebra.contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d = (CliffordAlgebra.contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>x : M<GOAL>(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>x : M<GOAL>(CliffordAlgebra.contractRight ((CliffordAlgebra.ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>r : R<GOAL>(CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>r : R<GOAL>(CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<GOAL>(CliffordAlgebra.contractLeft d) 1 = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<GOAL>(CliffordAlgebra.contractRight 1) d = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d) x) = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d') x) = -(CliffordAlgebra.contractLeft d') ((CliffordAlgebra.contractLeft d) x)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' = -(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>a : M<GOAL>∀ (a_1 : CliffordAlgebra Q), ((CliffordAlgebra.changeFormAux Q B) a) a_1 = (CliffordAlgebra.ι Q) a * a_1 - (CliffordAlgebra.contractLeft (B a)) a_1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>v : M<VAR>x : CliffordAlgebra Q<GOAL>((CliffordAlgebra.changeFormAux Q B) v) (((CliffordAlgebra.changeFormAux Q B) v) x) = (Q v - (B v) v) • x
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>LinearMap.BilinMap.toQuadraticMap 0 = Q - Q
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q'<GOAL>LinearMap.BilinMap.toQuadraticMap (B + B') = Q'' - Q
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<GOAL>LinearMap.BilinMap.toQuadraticMap (-B) = Q - Q'
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>Invertible 2<GOAL>(QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>r : R<GOAL>(CliffordAlgebra.changeForm h) ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q')) r
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<GOAL>(CliffordAlgebra.changeForm h) 1 = 1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>m : M<GOAL>(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q') m
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m * x) = (CliffordAlgebra.ι Q') m * (CliffordAlgebra.changeForm h) x - (CliffordAlgebra.contractLeft (B m)) ((CliffordAlgebra.changeForm h) x)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>m₁ m₂ : M<GOAL>(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂) = (CliffordAlgebra.ι Q') m₁ * (CliffordAlgebra.ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>d : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.changeForm h) ((CliffordAlgebra.contractLeft d) x) = (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.changeForm h) x)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.changeForm ⋯) x = x
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>CliffordAlgebra.changeForm ⋯ = LinearMap.id
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>x : CliffordAlgebra Q<GOAL>(CliffordAlgebra.changeForm h') ((CliffordAlgebra.changeForm h) x) = (CliffordAlgebra.changeForm ⋯) x
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q'<GOAL>CliffordAlgebra.changeForm h' ∘ₗ CliffordAlgebra.changeForm h = CliffordAlgebra.changeForm ⋯
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<VAR>a : CliffordAlgebra Q<GOAL>(CliffordAlgebra.changeFormEquiv h) a = (CliffordAlgebra.changeForm h) a
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>B : LinearMap.BilinForm R M<VAR>h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q<GOAL>(CliffordAlgebra.changeFormEquiv h).symm = CliffordAlgebra.changeFormEquiv ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : LinearMap.BilinForm R M<VAR>x : M<GOAL>(LinearMap.BilinForm.toLinHom A) x = A x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>α : Type u_7<VAR>t : Finset α<VAR>g : α → M<VAR>w : M<GOAL>(B (∑ i ∈ t, g i)) w = ∑ i ∈ t, (B (g i)) w
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>α : Type u_7<VAR>t : Finset α<VAR>w : M<VAR>g : α → M<GOAL>(B w) (∑ i ∈ t, g i) = ∑ i ∈ t, (B w) (g i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>α : Type u_7<VAR>t : Finset α<VAR>B : α → LinearMap.BilinForm R M<VAR>v w : M<GOAL>((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : LinearMap.BilinForm R M<VAR>x : M<GOAL>⇑((LinearMap.BilinForm.toLinHomFlip A) x) = fun y => (A y) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M →ₗ[R] R<GOAL>f.toBilinAux = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.toBilin.symm = LinearMap.BilinForm.toLin
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.toLin.symm = LinearMap.toBilin
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M →ₗ[R] R<VAR>x y : M<GOAL>((LinearMap.toBilin f) x) y = (f x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x : M<GOAL>(LinearMap.BilinForm.toLin B) x = B x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>R' : Type u_7<VAR>CommSemiring R'<VAR>Algebra R' R<VAR>Module R' M<VAR>IsScalarTower R' R M<VAR>f : R →ₗ[R'] R'<VAR>B : LinearMap.BilinForm R M<GOAL>∀ (a m : M), ((f.compBilinForm B) a) m = f ((B a) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>M'' : Type u_7<VAR>AddCommMonoid M''<VAR>Module R M''<VAR>B : LinearMap.BilinForm R M''<VAR>l r : M →ₗ[R] M'<VAR>l' r' : M' →ₗ[R] M''<GOAL>(B.comp l' r').comp l r = B.comp (l' ∘ₗ l) (r' ∘ₗ r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>l r : M →ₗ[R] M<GOAL>(B.compLeft l).compRight r = B.comp l r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>l r : M →ₗ[R] M<GOAL>(B.compRight r).compLeft l = B.comp l r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B : LinearMap.BilinForm R M'<VAR>l r : M →ₗ[R] M'<VAR>v w : M<GOAL>((B.comp l r) v) w = (B (l v)) (r w)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>f : M →ₗ[R] M<VAR>v w : M<GOAL>((B.compLeft f) v) w = (B (f v)) w
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>f : M →ₗ[R] M<VAR>v w : M<GOAL>((B.compRight f) v) w = (B v) (f w)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>r : M →ₗ[R] M<GOAL>B.comp LinearMap.id r = B.compRight r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>l : M →ₗ[R] M<GOAL>B.comp l LinearMap.id = B.compLeft l
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.compLeft LinearMap.id = B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.compRight LinearMap.id = B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.comp LinearMap.id LinearMap.id = B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type w<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>B₁ B₂ : LinearMap.BilinForm R M'<VAR>l r : M →ₗ[R] M'<VAR>hₗ : Function.Surjective ⇑l<VAR>hᵣ : Function.Surjective ⇑r<GOAL>B₁.comp l r = B₂.comp l r ↔ B₁ = B₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>e : M ≃ₗ[R] M'<VAR>B : LinearMap.BilinForm R M<VAR>x y : M'<GOAL>(((LinearMap.BilinForm.congr e) B) x) y = (B (e.symm x)) (e.symm y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>e : M ≃ₗ[R] M'<GOAL>(LinearMap.BilinForm.congr e).symm = LinearMap.BilinForm.congr e.symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.BilinForm.congr (LinearEquiv.refl R M) = LinearEquiv.refl R (LinearMap.BilinForm R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>AddCommMonoid M'<VAR>AddCommMonoid M''<VAR>Module R M'<VAR>Module R M''<VAR>e : M ≃ₗ[R] M'<VAR>f : M' ≃ₗ[R] M''<GOAL>LinearMap.BilinForm.congr e ≪≫ₗ LinearMap.BilinForm.congr f = LinearMap.BilinForm.congr (e ≪≫ₗ f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>AddCommMonoid M'<VAR>AddCommMonoid M''<VAR>Module R M'<VAR>Module R M''<VAR>e : M' ≃ₗ[R] M''<VAR>f : M ≃ₗ[R] M'<VAR>B : LinearMap.BilinForm R M<GOAL>(LinearMap.BilinForm.congr e) ((LinearMap.BilinForm.congr f) B) = (LinearMap.BilinForm.congr (f ≪≫ₗ e)) B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>AddCommMonoid M'<VAR>AddCommMonoid M''<VAR>Module R M'<VAR>Module R M''<VAR>e : M ≃ₗ[R] M'<VAR>B : LinearMap.BilinForm R M<VAR>l r : M'' →ₗ[R] M'<GOAL>((LinearMap.BilinForm.congr e) B).comp l r = B.comp (↑e.symm ∘ₗ l) (↑e.symm ∘ₗ r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>AddCommMonoid M'<VAR>AddCommMonoid M''<VAR>Module R M'<VAR>Module R M''<VAR>e : M' ≃ₗ[R] M''<VAR>B : LinearMap.BilinForm R M<VAR>l r : M' →ₗ[R] M<GOAL>(LinearMap.BilinForm.congr e) (B.comp l r) = B.comp (l ∘ₗ ↑e.symm) (r ∘ₗ ↑e.symm)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] R<VAR>x y : M<GOAL>((LinearMap.BilinForm.linMulLin f g) x) y = f x * g y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_7<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>f g : M →ₗ[R] R<VAR>l r : M' →ₗ[R] M<GOAL>(LinearMap.BilinForm.linMulLin f g).comp l r = LinearMap.BilinForm.linMulLin (f ∘ₗ l) (g ∘ₗ r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] R<VAR>l : M →ₗ[R] M<GOAL>(LinearMap.BilinForm.linMulLin f g).compLeft l = LinearMap.BilinForm.linMulLin (f ∘ₗ l) g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] R<VAR>r : M →ₗ[R] M<GOAL>(LinearMap.BilinForm.linMulLin f g).compRight r = LinearMap.BilinForm.linMulLin f (g ∘ₗ r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B F₂ : LinearMap.BilinForm R M<VAR>ι : Type u_9<VAR>b : Basis ι R M<VAR>h : ∀ (i j : ι), (B (b i)) (b j) = (F₂ (b i)) (b j)<GOAL>B = F₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>ι : Type u_9<VAR>b : Basis ι R M<VAR>x y : M<GOAL>((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B x) y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q<VAR>x : (i : ι) → Ms i<GOAL>((Submodule.piQuotientLift p q f hf) fun i => Submodule.Quotient.mk (x i)) = Submodule.Quotient.mk (((LinearMap.lsum R Ms R) f) x)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q<VAR>i : ι<VAR>x : Ms i ⧸ p i<GOAL>(Submodule.piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ⋯) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>Ns : ι → Type u_5<VAR>(i : ι) → AddCommGroup (Ns i)<VAR>(i : ι) → Module R (Ns i)<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>f : (i : ι) → Ms i →ₗ[R] Ns i<VAR>hf : ∀ (i : ι), p i ≤ LinearMap.ker (f i)<VAR>x : (i : ι) → Ms i<GOAL>(Submodule.quotientPiLift p f hf) (Submodule.Quotient.mk x) = fun i => (f i) (x i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<GOAL>Function.LeftInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<GOAL>Function.RightInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>x y : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p<GOAL>Submodule.quotientPi_aux.toFun p (x + y) = Submodule.quotientPi_aux.toFun p x + Submodule.quotientPi_aux.toFun p y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>r : R<VAR>x : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p<GOAL>Submodule.quotientPi_aux.toFun p (r • x) = (RingHom.id R) r • Submodule.quotientPi_aux.toFun p x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<GOAL>∀ (a : (i : ι) → Ms i ⧸ p i), (Submodule.quotientPi p).symm a = (Submodule.piQuotientLift p (Submodule.pi Set.univ p) LinearMap.single ⋯) a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>Ms : ι → Type u_3<VAR>(i : ι) → AddCommGroup (Ms i)<VAR>(i : ι) → Module R (Ms i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<GOAL>∀ (a : ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p) (i : ι), (Submodule.quotientPi p) a i = (Submodule.quotientPiLift p (fun i => (p i).mkQ) ⋯) a i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<VAR>x : M<GOAL>↑(f.quotKerEquivRange (Submodule.Quotient.mk x)) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<VAR>x : M<VAR>h : f x ∈ LinearMap.range f<GOAL>f.quotKerEquivRange.symm ⟨f x, h⟩ = (LinearMap.ker f).mkQ x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Submodule.comap p.subtype (p ⊓ p') ≤ LinearMap.ker (LinearMap.subToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Function.Injective ⇑(LinearMap.quotientInfToSupQuotient p p')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Function.Surjective ⇑(LinearMap.quotientInfToSupQuotient p p')