Commit 2023-12-06 13:34 dc62cf3f

View on Github →

feat: Add norm_one_add_smul. (#8681)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

added theorem Matrix.coeff_det_one_add_X_smul_one

added theorem Matrix.derivative_det_one_add_X_smul

added theorem Matrix.derivative_det_one_add_X_smul_aux

added theorem Matrix.det_one_add_X_smul

added theorem Matrix.det_one_add_smul

added theorem Matrix.eval_det_add_X_smul

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

added theorem Matrix.trace_submatrix_succ

Created Mathlib/RingTheory/NormTrace.lean

added theorem Algebra.norm_one_add_smul

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

added theorem matPolyEquiv_map_smul