Module

Algebra_isIntegral_trace_of_finiteDimensional.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isIntegral_trace_of_finiteDimensional

2 declarations indexed from sourceView source ↗

Module documentation

Algebra is Integral trace of finite Dimensional

Imports4

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Mathlib.RingTheory.Trace.Defs
Mathlib.Tactic.Ext

Imported by2

theorem

aeval_mulVec_of_mulVec_eq_smul

L31 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isIntegral_trace_of_finiteDimensional.IsIntegralTrace.aeval_mulVec_of_mulVec_eq_smul

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isIntegral_trace_of_finiteDimensional
open Polynomial Matrix
namespace IsIntegralTrace
open _root_.Algebra

Lean source · statement

theorem aeval_mulVec_of_mulVec_eq_smul {F : Type*} [Field F] {n : Type*} [Fintype n] [DecidableEq n]
    (M : Matrix n n F) (μ : F) (v : n → F) (hv : M *ᵥ v = μ • v) (p : F[X]) :
    (aeval M p) *ᵥ v = (p.eval μ) • v

theorem

isIntegral_trace_of_finiteDimensional

L47 ↗

Algebra.isIntegral_trace_of_finiteDimensional

Source context 4 commands