Commit 2026-07-27 08:26 1a1a7c15

fix(Tactic/NormDet): make norm_det proofs compatible with modules (#42119) The proofs produced by the norm_det / eval_det simproc (added in #42059) could not be checked from within a module because the generated proofs depended on kernel checking of equalities for definitions (Array.ofFn, and certEntry, certIterStepEntry from the Bird determinant certificate evaluator) which are not exposed. The existing tests in MathlibTest/matrix.lean did not detect this issue because it was not a module itself. This PR:

• Fixes the issues resulting from non-exposed definitions
• Makes the MathlibTest/matrix.lean file into a module
• Adds proofs for the determinants of Cartan matrices LinearAlgebra/Matrix/Cartan using norm_det - showing that the simrproc can be used in mathlib modules. The function normalizeDetFromEntries generated a proof which related the matrix array literal to Array.ofFn fun k => A k.divNat k.modNat by an unchecked =Q equality. This cannot be checked by the kernel because Array.ofFn is not exposed. The solution here is to use List.ofFn instead, which is exposed. Similarly, the functions certEntry and certIterStepEntry in the Bird determinant certificate evaluator relied on definitional unfolding of BirdDet.get and BirdDet.stepEntry which are not exposed. The generated proofs now use the unfolding lemmas BirdDet.get_eq and BirdDet.stepEntry_eq instead.