Commit 2023-06-20 16:16 f0848496

View on Github →

feat: port RingTheory.Trace (#5256)

depends on: #5266

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Trace.lean

added def Algebra.embeddingsMatrix

added def Algebra.embeddingsMatrixReindex

added theorem Algebra.embeddingsMatrixReindex_eq_vandermonde

added theorem Algebra.embeddingsMatrix_apply

added theorem Algebra.isIntegral_trace

added theorem Algebra.traceForm_apply

added theorem Algebra.traceForm_isSymm

added theorem Algebra.traceForm_toMatrix

added theorem Algebra.traceForm_toMatrix_powerBasis

added theorem Algebra.traceMatrix_apply

added theorem Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans

added theorem Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans

added theorem Algebra.traceMatrix_of_basis

added theorem Algebra.traceMatrix_of_basis_mulVec

added theorem Algebra.traceMatrix_of_matrix_mulVec

added theorem Algebra.traceMatrix_of_matrix_vecMul

added theorem Algebra.traceMatrix_reindex

added theorem Algebra.trace_algebraMap

added theorem Algebra.trace_algebraMap_of_basis

added theorem Algebra.trace_apply

added theorem Algebra.trace_comp_trace

added theorem Algebra.trace_comp_trace_of_basis

added theorem Algebra.trace_eq_matrix_trace

added theorem Algebra.trace_eq_zero_of_not_exists_basis

added theorem Algebra.trace_prod

added theorem Algebra.trace_prod_apply

added theorem Algebra.trace_trace

added theorem Algebra.trace_trace_of_basis

added theorem IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots

added theorem IntermediateField.AdjoinSimple.trace_gen_eq_zero

added theorem PowerBasis.trace_gen_eq_nextCoeff_minpoly

added theorem PowerBasis.trace_gen_eq_sum_roots

added theorem det_traceForm_ne_zero

added theorem det_traceMatrix_ne_zero'

added theorem sum_embeddings_eq_finrank_mul

added theorem traceForm_nondegenerate

added theorem trace_eq_sum_automorphisms

added theorem trace_eq_sum_embeddings

added theorem trace_eq_sum_embeddings_gen

added theorem trace_eq_sum_roots

added theorem trace_eq_trace_adjoin