Commit 2025-10-22 20:30 663fc8b3

View on Github →

feat(RingTheory): define the dual of a basis for the trace and prove basic properties (#26396) Specialize the construction of BilinForm.dualBasis to the case of the trace and proves basic results about it. This will be useful for future works on the Submodule.traceDual

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

modified theorem LinearMap.BilinForm.apply_dualBasis_left

modified theorem LinearMap.BilinForm.apply_dualBasis_right

modified theorem LinearMap.BilinForm.dualBasis_dualBasis

modified theorem LinearMap.BilinForm.dualBasis_dualBasis_flip

added theorem LinearMap.BilinForm.dualBasis_eq_iff

modified theorem LinearMap.BilinForm.dualBasis_flip_dualBasis

added theorem LinearMap.BilinForm.dualBasis_injective

added theorem LinearMap.BilinForm.dualBasis_involutive

modified theorem LinearMap.BilinForm.dualBasis_repr_apply

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem Submodule.traceDual_span_of_basis

Modified Mathlib/RingTheory/PowerBasis.lean

deleted def Module.Basis.PowerBasis

Modified Mathlib/RingTheory/Trace/Basic.lean

added theorem Algebra.isNilpotent_trace_of_isNilpotent

modified theorem Algebra.traceMatrix_of_basis_mulVec

deleted theorem Algebra.trace_isNilpotent_of_isNilpotent

added theorem Module.Basis.traceDual_def

added theorem Module.Basis.traceDual_eq_iff

added theorem Module.Basis.traceDual_inj

added theorem Module.Basis.traceDual_injective

added theorem Module.Basis.traceDual_involutive

added theorem Module.Basis.traceDual_powerBasis_eq

added theorem Module.Basis.traceDual_repr_apply

added theorem Module.Basis.traceDual_traceDual

added theorem Module.Basis.trace_mul_traceDual

added theorem Module.Basis.trace_traceDual_mul

modified theorem det_traceForm_ne_zero

deleted theorem traceForm_dualBasis_powerBasis_eq