Commit 2024-12-11 08:26 afdb9499

View on Github →

chore: renaming all Column to Col (#19825)

Matrix.fromColumns becomes Matrix.fromCols
Matrix.toColumns becomes Matrix.toCols
Matrix.updateColumn becomes Matrix.updateCol Moves:

*fromColumns* -> *fromCols*
*toColumns* -> *toCols*
*updateColumn* -> *updateCol* Discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Matrix.2EfromRows.20and.20Matrix.2EfromColumns

Estimated changes

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

added theorem Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose

deleted theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose

added theorem Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose

deleted theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose

added theorem Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm

deleted theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm

added def Matrix.fromCols

added theorem Matrix.fromCols_apply_inl

added theorem Matrix.fromCols_apply_inr

added theorem Matrix.fromCols_ext_iff

added theorem Matrix.fromCols_fromRows_eq_fromBlocks

added theorem Matrix.fromCols_inj

added theorem Matrix.fromCols_mulVec_sum_elim

added theorem Matrix.fromCols_mul_fromBlocks

added theorem Matrix.fromCols_mul_fromRows

added theorem Matrix.fromCols_mul_fromRows_eq_one_comm

added theorem Matrix.fromCols_neg

added theorem Matrix.fromCols_toCols

added theorem Matrix.fromCols_zero

deleted def Matrix.fromColumns

deleted theorem Matrix.fromColumns_apply_inl

deleted theorem Matrix.fromColumns_apply_inr

deleted theorem Matrix.fromColumns_ext_iff

deleted theorem Matrix.fromColumns_fromRows_eq_fromBlocks

deleted theorem Matrix.fromColumns_inj

deleted theorem Matrix.fromColumns_mulVec_sum_elim

deleted theorem Matrix.fromColumns_mul_fromBlocks

deleted theorem Matrix.fromColumns_mul_fromRows

deleted theorem Matrix.fromColumns_mul_fromRows_eq_one_comm

deleted theorem Matrix.fromColumns_neg

deleted theorem Matrix.fromColumns_toColumns

deleted theorem Matrix.fromColumns_zero

added theorem Matrix.fromRows_fromCols_eq_fromBlocks

deleted theorem Matrix.fromRows_fromColumn_eq_fromBlocks

added theorem Matrix.fromRows_mul_fromCols

deleted theorem Matrix.fromRows_mul_fromColumns

added theorem Matrix.mul_fromCols

deleted theorem Matrix.mul_fromColumns

added def Matrix.toCols₁

added theorem Matrix.toCols₁_apply

added theorem Matrix.toCols₁_fromCols

added def Matrix.toCols₂

added theorem Matrix.toCols₂_apply

added theorem Matrix.toCols₂_fromCols

deleted def Matrix.toColumns₁

deleted theorem Matrix.toColumns₁_apply

deleted theorem Matrix.toColumns₁_fromColumns

deleted def Matrix.toColumns₂

deleted theorem Matrix.toColumns₂_apply

deleted theorem Matrix.toColumns₂_fromColumns

added theorem Matrix.transpose_fromCols

deleted theorem Matrix.transpose_fromColumns

added theorem Matrix.vecMul_fromCols

deleted theorem Matrix.vecMul_fromColumns

Modified Mathlib/Data/Matrix/Notation.lean

added theorem Matrix.submatrix_updateCol_succAbove

deleted theorem Matrix.submatrix_updateColumn_succAbove

Modified Mathlib/Data/Matrix/RowCol.lean

added theorem Matrix.diagonal_updateCol_single

deleted theorem Matrix.diagonal_updateColumn_single

added theorem Matrix.map_updateCol

deleted theorem Matrix.map_updateColumn

added theorem Matrix.reindex_updateCol

deleted theorem Matrix.reindex_updateColumn

added theorem Matrix.submatrix_updateCol_equiv

deleted theorem Matrix.submatrix_updateColumn_equiv

added def Matrix.updateCol

added theorem Matrix.updateCol_apply

added theorem Matrix.updateCol_conjTranspose

added theorem Matrix.updateCol_eq_self

added theorem Matrix.updateCol_ne

added theorem Matrix.updateCol_reindex

added theorem Matrix.updateCol_self

added theorem Matrix.updateCol_submatrix_equiv

added theorem Matrix.updateCol_subsingleton

added theorem Matrix.updateCol_transpose

deleted def Matrix.updateColumn

deleted theorem Matrix.updateColumn_apply

deleted theorem Matrix.updateColumn_conjTranspose

deleted theorem Matrix.updateColumn_eq_self

deleted theorem Matrix.updateColumn_ne

deleted theorem Matrix.updateColumn_reindex

deleted theorem Matrix.updateColumn_self

deleted theorem Matrix.updateColumn_submatrix_equiv

deleted theorem Matrix.updateColumn_subsingleton

deleted theorem Matrix.updateColumn_transpose

modified theorem Matrix.updateRow_transpose

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

modified theorem Matrix.cramer_apply

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

added theorem Matrix.det_updateCol_add

added theorem Matrix.det_updateCol_add_self

added theorem Matrix.det_updateCol_add_smul_self

added theorem Matrix.det_updateCol_eq_zero

added theorem Matrix.det_updateCol_smul

added theorem Matrix.det_updateCol_smul_left

added theorem Matrix.det_updateCol_sum

deleted theorem Matrix.det_updateColumn_add

deleted theorem Matrix.det_updateColumn_add_self

deleted theorem Matrix.det_updateColumn_add_smul_self

deleted theorem Matrix.det_updateColumn_eq_zero

deleted theorem Matrix.det_updateColumn_smul

deleted theorem Matrix.det_updateColumn_smul_left

deleted theorem Matrix.det_updateColumn_sum

Modified Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

added theorem Matrix.fromCols_col0_isTotallyUnimodular_iff

added theorem Matrix.fromCols_one_isTotallyUnimodular_iff

deleted theorem Matrix.fromColumns_col0_isTotallyUnimodular_iff

deleted theorem Matrix.fromColumns_one_isTotallyUnimodular_iff

added theorem Matrix.one_fromCols_isTotallyUnimodular_iff

deleted theorem Matrix.one_fromColumns_isTotallyUnimodular_iff

Modified Mathlib/LinearAlgebra/Matrix/Permanent.lean

added theorem Matrix.permanent_updateCol_smul

deleted theorem Matrix.permanent_updateColumn_smul

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/Topology/Instances/Matrix.lean

added theorem Continuous.matrix_updateCol

deleted theorem Continuous.matrix_updateColumn

Modified scripts/nolints_prime_decls.txt