ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>k : σ → τ<VAR>p : MvPolynomial σ R<VAR>g : τ → MvPolynomial σ R<GOAL>(MvPolynomial.rename k) (MvPolynomial.eval₂ MvPolynomial.C (g ∘ k) p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.rename k) ∘ g) ((MvPolynomial.rename k) p)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>j : τ<VAR>g : σ → MvPolynomial σ R<GOAL>(MvPolynomial.rename (Prod.mk j)) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (fun x => (MvPolynomial.rename (Prod.mk j)) (g x)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>g : σ × τ → S<VAR>i : σ<VAR>p : MvPolynomial τ R<GOAL>MvPolynomial.eval₂ f g ((MvPolynomial.rename (Prod.mk i)) p) = MvPolynomial.eval₂ f (fun j => g (i, j)) p
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>g : σ × τ → R<VAR>i : σ<VAR>p : MvPolynomial τ R<GOAL>(MvPolynomial.eval g) ((MvPolynomial.rename (Prod.mk i)) p) = (MvPolynomial.eval fun j => g (i, j)) p
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>∃ s q, p = (MvPolynomial.rename Subtype.val) q
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p₁ p₂ : MvPolynomial σ R<GOAL>∃ s q₁ q₂, p₁ = (MvPolynomial.rename Subtype.val) q₁ ∧ p₂ = (MvPolynomial.rename Subtype.val) q₂
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>∃ n f, ∃ (_ : Function.Injective f), ∃ q, p = (MvPolynomial.rename f) q
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>c : ℤ →+* R<VAR>g : τ → R<VAR>p : MvPolynomial σ ℤ<GOAL>MvPolynomial.eval₂ c (g ∘ f) p = MvPolynomial.eval₂ c g ((MvPolynomial.rename f) p)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>hf : Function.Injective f<VAR>φ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff (Finsupp.mapDomain f d) ((MvPolynomial.rename f) φ) = MvPolynomial.coeff d φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ ↪ τ<VAR>φ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff (Finsupp.embDomain f d) ((MvPolynomial.rename ⇑f) φ) = MvPolynomial.coeff d φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>d : τ →₀ ℕ<VAR>h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → MvPolynomial.coeff u φ = 0<GOAL>MvPolynomial.coeff d ((MvPolynomial.rename f) φ) = 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>d : τ →₀ ℕ<VAR>h : MvPolynomial.coeff d ((MvPolynomial.rename f) φ) ≠ 0<GOAL>∃ u, Finsupp.mapDomain f u = d ∧ MvPolynomial.coeff u φ ≠ 0
<VAR>σ : Type u_1<VAR>R : Type u_4<VAR>CommSemiring R<VAR>τ : Type u_6<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.constantCoeff ((MvPolynomial.rename f) φ) = MvPolynomial.constantCoeff φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_4<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>f : σ → τ<VAR>DecidableEq τ<VAR>h : Function.Injective f<GOAL>((MvPolynomial.rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>f : σ → A<VAR>s : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.mkDerivationₗ R f) ((MvPolynomial.monomial s) r) = r • s.sum fun i k => (MvPolynomial.monomial (s - Finsupp.single i 1)) ↑k • f i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>f : σ → A<VAR>r : R<GOAL>(MvPolynomial.mkDerivationₗ R f) (MvPolynomial.C r) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>f : σ → A<VAR>i : σ<GOAL>(MvPolynomial.mkDerivationₗ R f) (MvPolynomial.X i) = f i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D : Derivation R (MvPolynomial σ R) A<VAR>a : R<GOAL>D (MvPolynomial.C a) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D : Derivation R (MvPolynomial σ R) A<VAR>a : R<VAR>f : MvPolynomial σ R<GOAL>MvPolynomial.C a • D f = a • D f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D₁ D₂ : Derivation R (MvPolynomial σ R) A<VAR>s : Set σ<VAR>h : Set.EqOn (⇑D₁ ∘ MvPolynomial.X) (⇑D₂ ∘ MvPolynomial.X) s<VAR>f : MvPolynomial σ R<VAR>hf : f ∈ MvPolynomial.supported R s<GOAL>D₁ f = D₂ f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D₁ D₂ : Derivation R (MvPolynomial σ R) A<VAR>f : MvPolynomial σ R<VAR>h : ∀ i ∈ f.vars, D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)<GOAL>D₁ f = D₂ f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D : Derivation R (MvPolynomial σ R) A<VAR>f : MvPolynomial σ R<VAR>h : ∀ i ∈ f.vars, D (MvPolynomial.X i) = 0<GOAL>D f = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>D₁ D₂ : Derivation R (MvPolynomial σ R) A<VAR>h : ∀ (i : σ), D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)<GOAL>D₁ = D₂
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>IsScalarTower R (MvPolynomial σ R) A<VAR>D : MvPolynomial σ R →ₗ[R] A<VAR>h₁ : D 1 = 0<GOAL>(∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p) ↔ ∀ (s : σ →₀ ℕ) (i : σ), D ((MvPolynomial.monomial s) 1 * MvPolynomial.X i) = (MvPolynomial.monomial s) 1 • D (MvPolynomial.X i) + MvPolynomial.X i • D ((MvPolynomial.monomial s) 1)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>IsScalarTower R (MvPolynomial σ R) A<VAR>f : σ → A<VAR>i : σ<GOAL>(MvPolynomial.mkDerivation R f) (MvPolynomial.X i) = f i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Module (MvPolynomial σ R) A<VAR>IsScalarTower R (MvPolynomial σ R) A<VAR>f : σ → A<VAR>s : σ →₀ ℕ<VAR>r : R<GOAL>(MvPolynomial.mkDerivation R f) ((MvPolynomial.monomial s) r) = r • s.sum fun i k => (MvPolynomial.monomial (s - Finsupp.single i 1)) ↑k • f i
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>Star R<VAR>self : StarSubsemiring R<VAR>a : R<GOAL>a ∈ self.carrier → star a ∈ self.carrier
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>s : StarSubsemiring R<VAR>x : R<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S T : StarSubsemiring R<VAR>h : ∀ (x : R), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S : Subsemiring R<VAR>h : ∀ {a : R}, a ∈ S.carrier → star a ∈ S.carrier<GOAL>↑{ toSubsemiring := S, star_mem' := h } = ↑S
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S : StarSubsemiring R<VAR>x : R<GOAL>x ∈ S.toSubsemiring ↔ x ∈ S
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S : StarSubsemiring R<GOAL>↑S.toSubsemiring = ↑S
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<GOAL>Function.Injective StarSubsemiring.toSubsemiring
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S U : StarSubsemiring R<GOAL>S.toSubsemiring = U.toSubsemiring ↔ S = U
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S₁ S₂ : StarSubsemiring R<GOAL>S₁.toSubsemiring ≤ S₂.toSubsemiring ↔ S₁ ≤ S₂
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S : StarSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type v<VAR>NonAssocSemiring R<VAR>StarRing R<VAR>S : StarSubsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>M : Matrix m n R<VAR>i : m<VAR>c : n → R<GOAL>(MvPolynomial.eval c) (M.toMvPolynomial i) = (M *ᵥ c) i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Fintype n<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R →+* S<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.toMvPolynomial i).IsHomogeneous 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>M : Matrix m n R<VAR>i : m<GOAL>(M.toMvPolynomial i).totalDegree ≤ 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>M : Matrix m n R<VAR>i : m<GOAL>MvPolynomial.constantCoeff (M.toMvPolynomial i) = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<GOAL>Matrix.toMvPolynomial 0 = 0
<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>DecidableEq n<GOAL>Matrix.toMvPolynomial 1 = MvPolynomial.X
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_4<VAR>Fintype n<VAR>CommSemiring R<VAR>M N : Matrix m n R<GOAL>(M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>Fintype n<VAR>Fintype o<VAR>CommSemiring R<VAR>M : Matrix m n R<VAR>N : Matrix n o R<VAR>i : m<GOAL>(M * N).toMvPolynomial i = (MvPolynomial.bind₁ N.toMvPolynomial) (M.toMvPolynomial i)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<VAR>c : ι₁ →₀ R<GOAL>(MvPolynomial.eval ⇑c) (LinearMap.toMvPolynomial b₁ b₂ f i) = (b₂.repr (f (b₁.repr.symm c))) i
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<VAR>A : Type u_6<VAR>CommRing A<VAR>Algebra R A<GOAL>LinearMap.toMvPolynomial (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂) (LinearMap.baseChange A f) i = (MvPolynomial.map (algebraMap R A)) (LinearMap.toMvPolynomial b₁ b₂ f i)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<GOAL>(LinearMap.toMvPolynomial b₁ b₂ f i).IsHomogeneous 1
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<GOAL>(LinearMap.toMvPolynomial b₁ b₂ f i).totalDegree ≤ 1
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₂<GOAL>MvPolynomial.constantCoeff (LinearMap.toMvPolynomial b₁ b₂ f i) = 0
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>LinearMap.toMvPolynomial b₁ b₂ 0 = 0
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>ι₁ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Fintype ι₁<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<GOAL>LinearMap.toMvPolynomial b₁ b₁ LinearMap.id = MvPolynomial.X
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Finite ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f g : M₁ →ₗ[R] M₂<GOAL>LinearMap.toMvPolynomial b₁ b₂ (f + g) = LinearMap.toMvPolynomial b₁ b₂ f + LinearMap.toMvPolynomial b₁ b₂ g
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>ι₁ : Type u_5<VAR>ι₂ : Type u_6<VAR>ι₃ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>Finite ι₃<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>b₃ : Basis ι₃ R M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>f : M₁ →ₗ[R] M₂<VAR>i : ι₃<GOAL>LinearMap.toMvPolynomial b₁ b₃ (g ∘ₗ f) i = (MvPolynomial.bind₁ (LinearMap.toMvPolynomial b₁ b₂ f)) (LinearMap.toMvPolynomial b₂ b₃ g i)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>A : Type u_8<VAR>CommRing A<VAR>Algebra R A<GOAL>(LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpolyAux (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A bₘ) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b bₘ)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>x : L<VAR>i : ℕ<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = ((LinearMap.toMatrix bₘ bₘ) (φ x)).charpoly.coeff i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : L<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : L<VAR>i : ℕ<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (LinearMap.charpoly (φ x)).coeff i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>Module.Finite R M<VAR>Module.Free R M<VAR>x : ι → R<GOAL>Polynomial.map (MvPolynomial.eval x) (φ.polyCharpolyAux b bₘ) = LinearMap.charpoly (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x)))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>A : Type u_8<VAR>CommRing A<VAR>Algebra R A<VAR>Module.Finite A (TensorProduct R A M)<VAR>Module.Free A (TensorProduct R A M)<VAR>x : ι → A<GOAL>Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) = ((LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ) ((Algebra.TensorProduct.basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>Fintype ιM'<VAR>DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<GOAL>φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ιM : Type u_7<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ιM<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>DecidableEq ιM<VAR>bₘ : Basis ιM R M<GOAL>φ.polyCharpoly b = Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<GOAL>(φ.polyCharpoly b).Monic
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>Nontrivial R<GOAL>φ.polyCharpoly b ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>Nontrivial R<GOAL>(φ.polyCharpoly b).natDegree = FiniteDimensional.finrank R M
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>i j : ℕ<VAR>hij : i + j = FiniteDimensional.finrank R M<VAR>Nontrivial R<GOAL>((φ.polyCharpoly b).coeff i).IsHomogeneous j
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>A : Type u_8<VAR>CommRing A<VAR>Algebra R A<GOAL>(LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ).polyCharpoly (Algebra.TensorProduct.basis A b) = Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>x : L<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = LinearMap.charpoly (φ x)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>x : L<VAR>i : ℕ<GOAL>(MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (LinearMap.charpoly (φ x)).coeff i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ι'<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<VAR>H : (φ.polyCharpoly b).coeff k = 0<GOAL>(φ.polyCharpoly b').coeff k = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ι'<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<GOAL>(φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>Nontrivial R<GOAL>(φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ι'<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>φ.nilRankAux b ≤ φ.nilRankAux b'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Fintype ι'<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>b : Basis ι R L<GOAL>φ.nilRank = (φ.polyCharpoly b).natTrailingDegree
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>b : Basis ι R L<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<GOAL>(φ.polyCharpoly b).coeff φ.nilRank ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Fintype ι<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<VAR>b : Basis ι R M<GOAL>φ.nilRank ≤ Fintype.card ι
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup L<VAR>Module R L<VAR>AddCommGroup M<VAR>Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>Module.Finite R L<VAR>Module.Free R L<VAR>Nontrivial R<GOAL>φ.nilRank ≤ FiniteDimensional.finrank R M