Commit 2026-06-29 22:55 cb4d969b

View on Github →

feat(LinearAlgebra): fill two proof_wanted declarations (#39046) ... and generalize AlgHom.bijective and move to earlier file.

Estimated changes

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Matrix.det_map'

Modified Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

added theorem AlgHom.bijective

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem Matrix.trace_map'

Modified Mathlib/RingTheory/Algebraic/Integral.lean

deleted theorem AlgHom.bijective