ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>⇑(LinearMap.quotientInfToSupQuotient p p') = ⇑(LinearMap.quotientInfEquivSupQuotient 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<VAR>x : ↥p<GOAL>let map := Submodule.inclusion ⋯;
(LinearMap.quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk x) = Submodule.Quotient.mk (map 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<VAR>x : ↥(p ⊔ p')<VAR>hx : ↑x ∈ p<GOAL>(LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, hx⟩
<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<VAR>x : ↥(p ⊔ p')<GOAL>(LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ ↑x ∈ 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<VAR>x : ↥(p ⊔ p')<VAR>hx : ↑x ∈ p'<GOAL>(LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<VAR>h : S ≤ T<VAR>x : M ⧸ S<GOAL>(S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk x) = (S.mapQ T LinearMap.id h) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<VAR>h : S ≤ T<VAR>x : M<GOAL>(S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk (Submodule.Quotient.mk x)) = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S T : Submodule R M<VAR>hST : T ≤ S<GOAL>Nat.card ↥(Submodule.map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)
<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>m : M × R<GOAL>(CliffordAlgebra.EquivEven.Q' Q) m = Q m.1 - m.2 * m.2
<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>m : M<VAR>r : R<GOAL>(CliffordAlgebra.ι (CliffordAlgebra.EquivEven.Q' Q)) (m, r) = (CliffordAlgebra.EquivEven.v Q) m + r • CliffordAlgebra.EquivEven.e0 Q
<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<GOAL>CliffordAlgebra.EquivEven.e0 Q * CliffordAlgebra.EquivEven.e0 Q = -1
<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>m : M<GOAL>(CliffordAlgebra.EquivEven.v Q) m * (CliffordAlgebra.EquivEven.v Q) m = (algebraMap R (CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q))) (Q m)
<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>m : M<GOAL>-(CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m) = (CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q
<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>m : M<GOAL>-((CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q) = CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m
<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>m : M<GOAL>CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q = (CliffordAlgebra.EquivEven.v Q) m
<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>m : M<GOAL>CliffordAlgebra.reverse ((CliffordAlgebra.EquivEven.v Q) m) = (CliffordAlgebra.EquivEven.v Q) m
<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>m : M<GOAL>CliffordAlgebra.involute ((CliffordAlgebra.EquivEven.v Q) m) = -(CliffordAlgebra.EquivEven.v Q) m
<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<GOAL>CliffordAlgebra.reverse (CliffordAlgebra.EquivEven.e0 Q) = CliffordAlgebra.EquivEven.e0 Q
<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<GOAL>CliffordAlgebra.involute (CliffordAlgebra.EquivEven.e0 Q) = -CliffordAlgebra.EquivEven.e0 Q
<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>m : M<GOAL>↑((CliffordAlgebra.toEven Q) ((CliffordAlgebra.ι Q) m)) = CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m
<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>x y : M × R<GOAL>(CliffordAlgebra.ofEven Q) (((CliffordAlgebra.even.ι (CliffordAlgebra.EquivEven.Q' Q)).bilin x) y) = ((CliffordAlgebra.ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((CliffordAlgebra.ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
<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<GOAL>(CliffordAlgebra.toEven Q).comp (CliffordAlgebra.ofEven Q) = AlgHom.id R ↥(CliffordAlgebra.even (CliffordAlgebra.EquivEven.Q' Q))
<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<GOAL>(CliffordAlgebra.ofEven Q).comp (CliffordAlgebra.toEven Q) = AlgHom.id R (CliffordAlgebra Q)
<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>x : CliffordAlgebra Q<GOAL>↑((CliffordAlgebra.toEven Q) (CliffordAlgebra.reverse (CliffordAlgebra.involute x))) = CliffordAlgebra.reverse ↑((CliffordAlgebra.toEven Q) x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>h : Q' = -Q<VAR>m₁ m₂ : M<GOAL>(CliffordAlgebra.evenToNeg Q Q' h) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = -((CliffordAlgebra.even.ι Q').bilin m₁) m₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q Q' : QuadraticForm R M<VAR>h : Q' = -Q<VAR>h' : Q = -Q'<GOAL>(CliffordAlgebra.evenToNeg Q' Q h').comp (CliffordAlgebra.evenToNeg Q Q' h) = AlgHom.id R ↥(CliffordAlgebra.even Q)
<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>a : ↥(CliffordAlgebra.even (-Q))<GOAL>(CliffordAlgebra.evenEquivEvenNeg Q).symm a = (CliffordAlgebra.evenToNeg (-Q) Q ⋯) a
<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>a : ↥(CliffordAlgebra.even Q)<GOAL>(CliffordAlgebra.evenEquivEvenNeg Q) a = (CliffordAlgebra.evenToNeg Q (-Q) ⋯) a
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing R<VAR>CharZero R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>a b : P<GOAL>(AffineMap.lineMap a b) 2⁻¹ = midpoint R a b
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing R<VAR>CharZero R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>a b : P<GOAL>(AffineMap.lineMap a b) (1 / 2) = midpoint R a b
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>CommRing R<VAR>Invertible 2<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>a b : P<GOAL>(AffineMap.homothety a ⅟2) b = midpoint R a b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Field k<VAR>CharZero k<VAR>AddCommGroup V<VAR>Module k V<VAR>AddTorsor V P<VAR>a b : P<GOAL>(AffineMap.homothety a 2⁻¹) b = midpoint k a b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Field k<VAR>CharZero k<VAR>AddCommGroup V<VAR>Module k V<VAR>AddTorsor V P<VAR>a b : P<GOAL>(AffineMap.homothety a (1 / 2)) b = midpoint k a b
<VAR>k : Type u_1<VAR>ι : Type u_2<VAR>V : ι → Type u_3<VAR>P : ι → Type u_4<VAR>Field k<VAR>Invertible 2<VAR>(i : ι) → AddCommGroup (V i)<VAR>(i : ι) → Module k (V i)<VAR>(i : ι) → AddTorsor (V i) (P i)<VAR>f g : (i : ι) → P i<VAR>i : ι<GOAL>midpoint k f g i = midpoint k (f i) (g i)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<GOAL>slope f = fun a b => (b - a)⁻¹ • (f b -ᵥ f a)
<VAR>k : Type u_1<VAR>Field k<VAR>f : k → k<VAR>a b : k<GOAL>slope f a b = (f b - f a) / (b - a)
<VAR>k : Type u_1<VAR>Field k<VAR>f : k → k<VAR>a : k<GOAL>slope f a = fun b => (f b - f a) / (b - a)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a : k<GOAL>slope f a a = 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>f : k → E<VAR>a b : k<GOAL>slope f a b = (b - a)⁻¹ • (f b - f a)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>(b - a) • slope f a b = f b -ᵥ f a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>(b - a) • slope f a b +ᵥ f a = f b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → E<VAR>c : PE<GOAL>(slope fun x => f x +ᵥ c) = slope f
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>f : k → E<VAR>a b : k<VAR>h : a ≠ b<GOAL>slope (fun x => (x - a) • f x) a b = f b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<VAR>h : slope f a b = 0<GOAL>f a = f b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>F : Type u_4<VAR>PF : Type u_5<VAR>AddCommGroup F<VAR>Module k F<VAR>AddTorsor F PF<VAR>f : PE →ᵃ[k] PF<VAR>g : k → PE<VAR>a b : k<GOAL>slope (⇑f ∘ g) a b = f.linear (slope g a b)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>F : Type u_4<VAR>AddCommGroup F<VAR>Module k F<VAR>f : E →ₗ[k] F<VAR>g : k → E<VAR>a b : k<GOAL>slope (⇑f ∘ g) a b = f (slope g a b)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<GOAL>slope f a b = slope f b a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>f : k → E<VAR>x y : k<GOAL>slope (fun t => -f t) x y = -slope f x y
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>f : k → E<GOAL>slope (-f) = -slope f
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b c : k<GOAL>((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b c : k<VAR>h : a ≠ c<GOAL>(AffineMap.lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>Field k<VAR>AddCommGroup E<VAR>Module k E<VAR>AddTorsor E PE<VAR>f : k → PE<VAR>a b r : k<GOAL>(AffineMap.lineMap (slope f ((AffineMap.lineMap a b) r) b) (slope f a ((AffineMap.lineMap a b) r))) r = slope f a b
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ x ∈ s, Polynomial.eval x f = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f.degree < ↑s.card<VAR>degree_g_lt : g.degree < ↑s.card<VAR>eval_fg : ∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ i ∈ s, Polynomial.eval (v i) f = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_fg_lt : (f - g).degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>degree_g_lt : g.degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>h_deg_le : f.degree ≤ ↑s.card<VAR>h_deg_eq : f.degree = g.degree<VAR>hlc : f.leadingCoeff = g.leadingCoeff<VAR>h_eval : ∀ i ∈ s, Polynomial.eval (v i) f = Polynomial.eval (v i) g<GOAL>f = g
<VAR>F : Type u_1<VAR>Field F<VAR>x : F<GOAL>Lagrange.basisDivisor x x = 0
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<VAR>hxy : Lagrange.basisDivisor x y = 0<GOAL>x = y
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<GOAL>Lagrange.basisDivisor x y = 0 ↔ x = y
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<GOAL>Lagrange.basisDivisor x y ≠ 0 ↔ x ≠ y
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>(Lagrange.basisDivisor x y).degree = 1
<VAR>F : Type u_1<VAR>Field F<VAR>x : F<GOAL>(Lagrange.basisDivisor x x).degree = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>x : F<GOAL>(Lagrange.basisDivisor x x).natDegree = 0
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>(Lagrange.basisDivisor x y).natDegree = 1
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<GOAL>Polynomial.eval y (Lagrange.basisDivisor x y) = 0
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>Polynomial.eval x (Lagrange.basisDivisor x y) = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>v : ι → F<VAR>i : ι<GOAL>Lagrange.basis ∅ v i = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>v : ι → F<VAR>i : ι<GOAL>Lagrange.basis {i} v i = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>Lagrange.basis {i, j} v i = Lagrange.basisDivisor (v i) (v j)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>Lagrange.basis {i, j} v j = Lagrange.basisDivisor (v j) (v i)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>Lagrange.basis s v i ≠ 0
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>Polynomial.eval (v i) (Lagrange.basis s v i) = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<VAR>hj : j ∈ s<GOAL>Polynomial.eval (v j) (Lagrange.basis s v i) = 0
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>(Lagrange.basis s v i).natDegree = s.card - 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>(Lagrange.basis s v i).degree = ↑(s.card - 1)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<GOAL>∑ j ∈ s, Lagrange.basis s v j = 1
<VAR>F : Type u_1<VAR>Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>Lagrange.basisDivisor x y + Lagrange.basisDivisor y x = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<GOAL>(Lagrange.interpolate s v) r = ∑ i ∈ s, Polynomial.C (r i) * Lagrange.basis s v i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>v : ι → F<VAR>r : ι → F<GOAL>(Lagrange.interpolate ∅ v) r = 0
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>i : ι<VAR>v : ι → F<VAR>r : ι → F<GOAL>(Lagrange.interpolate {i} v) r = Polynomial.C (r i)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hs : s.Nonempty<GOAL>(Lagrange.interpolate s v) 1 = 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>i : ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>Polynomial.eval (v i) ((Lagrange.interpolate s v) r) = r i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>((Lagrange.interpolate s v) r).degree ≤ ↑(s.card - 1)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>((Lagrange.interpolate s v) r).degree < ↑s.card
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>i : ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>((Lagrange.interpolate (s.erase i) v) r).degree < ↑(s.card - 1)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hrr' : (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r'<VAR>i : ι<GOAL>i ∈ s → r i = r' i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r r' : ι → F<VAR>hrr' : ∀ i ∈ s, r i = r' i<GOAL>(Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r'
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<GOAL>(Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r' ↔ ∀ i ∈ s, r i = r' i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>f : F[X]<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<GOAL>f = (Lagrange.interpolate s v) fun i => Polynomial.eval (v i) f
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>f : F[X]<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ i ∈ s, Polynomial.eval (v i) f = r i<GOAL>f = (Lagrange.interpolate s v) r
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>f : F[X]<VAR>hvs : Set.InjOn v ↑s<GOAL>(f.degree < ↑s.card ∧ ∀ i ∈ s, Polynomial.eval (v i) f = r i) ↔ f = (Lagrange.interpolate s v) r
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvt : Set.InjOn v ↑t<VAR>hs : s.Nonempty<VAR>hst : s ⊆ t<GOAL>(Lagrange.interpolate t v) r = ∑ i ∈ s, (Lagrange.interpolate (insert i (t \ s)) v) r * Lagrange.basis s v i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>i j : ι<VAR>v : ι → F<VAR>r : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hij : i ≠ j<GOAL>(Lagrange.interpolate s v) r = (Lagrange.interpolate (s.erase j) v) r * Lagrange.basisDivisor (v i) (v j) + (Lagrange.interpolate (s.erase i) v) r * Lagrange.basisDivisor (v j) (v i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<GOAL>Lagrange.nodal s v = ∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>v : ι → R<GOAL>Lagrange.nodal ∅ v = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>Nontrivial R<GOAL>(Lagrange.nodal s v).natDegree = s.card
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>Nontrivial R<GOAL>Lagrange.nodal s v ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>Nontrivial R<GOAL>(Lagrange.nodal s v).degree = ↑s.card
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<GOAL>(Lagrange.nodal s v).Monic
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>x : R<GOAL>Polynomial.eval x (Lagrange.nodal s v) = ∏ i ∈ s, (x - v i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Polynomial.eval (v i) (Lagrange.nodal s v) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>Nontrivial R<VAR>NoZeroDivisors R<VAR>x : R<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>Polynomial.eval x (Lagrange.nodal s v) ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Lagrange.nodal s v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal (s.erase i) v
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Polynomial.X - Polynomial.C (v i) ∣ Lagrange.nodal s v
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>Lagrange.nodal (insert i s) v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal s v
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>DecidableEq ι<GOAL>Polynomial.derivative (Lagrange.nodal s v) = ∑ i ∈ s, Lagrange.nodal (s.erase i) v
<VAR>R : Type u_1<VAR>CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)) = Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>G : Subgroup Rˣ<VAR>Fintype ↥G<GOAL>Lagrange.nodal (↑G).toFinset Units.val = Polynomial.X ^ Fintype.card ↥G - 1
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<GOAL>Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v))⁻¹
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Lagrange.nodal (s.erase i) v = Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)))⁻¹
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>Lagrange.nodalWeight s v i ≠ 0
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>Lagrange.basis s v i = Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i)))
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>x : F<VAR>hi : i ∈ s<VAR>hxi : x ≠ v i<GOAL>Polynomial.eval x (Lagrange.basis s v i) = Polynomial.eval x (Lagrange.nodal s v) * (Lagrange.nodalWeight s v i * (x - v i)⁻¹)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<GOAL>(Lagrange.interpolate s v) r = ∑ i ∈ s, Polynomial.C (Lagrange.nodalWeight s v i) * (Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))) * Polynomial.C (r i)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>r : ι → F<VAR>x : F<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>Polynomial.eval x ((Lagrange.interpolate s v) r) = Polynomial.eval x (Lagrange.nodal s v) * ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>x : F<VAR>hvs : Set.InjOn v ↑s<VAR>hx : ∀ i ∈ s, x ≠ v i<VAR>hs : s.Nonempty<GOAL>∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ ≠ 0