Commit 2024-11-28 16:12 2b0dc338

View on Github →

feat: drop finite-dimensionality assumption from PerfectPairing.restrictScalarsField (#18940)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.submatrix_id_mul_left

added theorem Matrix.submatrix_id_mul_right

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem Basis.dualBasis_repr

Created Mathlib/LinearAlgebra/Matrix/BaseChange.lean

added theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left

added theorem Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

added theorem Basis.toMatrix_mulVec_repr

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

added def PerfectPairing.dual

added theorem PerfectPairing.exists_basis_basis_of_span_eq_top_of_mem_algebraMap

added theorem PerfectPairing.finrank_eq

modified def PerfectPairing.restrictScalarsField

Modified docs/references.bib