Commit 2024-11-05 06:46 48832f00

View on Github →

chore: split Data.Matrix.ConjTranspose from Basic (#18643) Possible next steps:

Split RowCol/Invertible/Block to delay the star stuff
Invert the import order, moving star stuff from RowCol/Invertible/Block into ConjTranspose

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matrix/Basic.lean

deleted def Matrix.conjTranspose

deleted def Matrix.conjTransposeAddEquiv

deleted theorem Matrix.conjTransposeAddEquiv_symm

deleted def Matrix.conjTransposeLinearEquiv

deleted theorem Matrix.conjTransposeLinearEquiv_symm

deleted def Matrix.conjTransposeRingEquiv

deleted theorem Matrix.conjTranspose_add

deleted theorem Matrix.conjTranspose_apply

deleted theorem Matrix.conjTranspose_conjTranspose

deleted theorem Matrix.conjTranspose_eq_diagonal

deleted theorem Matrix.conjTranspose_eq_intCast

deleted theorem Matrix.conjTranspose_eq_natCast

deleted theorem Matrix.conjTranspose_eq_ofNat

deleted theorem Matrix.conjTranspose_eq_one

deleted theorem Matrix.conjTranspose_eq_transpose_of_trivial

deleted theorem Matrix.conjTranspose_eq_zero

deleted theorem Matrix.conjTranspose_inj

deleted theorem Matrix.conjTranspose_injective

deleted theorem Matrix.conjTranspose_intCast

deleted theorem Matrix.conjTranspose_intCast_smul

deleted theorem Matrix.conjTranspose_inv_intCast_smul

deleted theorem Matrix.conjTranspose_inv_natCast_smul

deleted theorem Matrix.conjTranspose_inv_ofNat_smul

deleted theorem Matrix.conjTranspose_list_prod

deleted theorem Matrix.conjTranspose_list_sum

deleted theorem Matrix.conjTranspose_map

deleted theorem Matrix.conjTranspose_mul

deleted theorem Matrix.conjTranspose_multiset_sum

deleted theorem Matrix.conjTranspose_natCast

deleted theorem Matrix.conjTranspose_natCast_smul

deleted theorem Matrix.conjTranspose_neg

deleted theorem Matrix.conjTranspose_nsmul

deleted theorem Matrix.conjTranspose_ofNat

deleted theorem Matrix.conjTranspose_ofNat_smul

deleted theorem Matrix.conjTranspose_one

deleted theorem Matrix.conjTranspose_pow

deleted theorem Matrix.conjTranspose_ratCast_smul

deleted theorem Matrix.conjTranspose_rat_smul

deleted theorem Matrix.conjTranspose_reindex

deleted theorem Matrix.conjTranspose_smul

deleted theorem Matrix.conjTranspose_smul_non_comm

deleted theorem Matrix.conjTranspose_smul_self

deleted theorem Matrix.conjTranspose_sub

deleted theorem Matrix.conjTranspose_submatrix

deleted theorem Matrix.conjTranspose_sum

deleted theorem Matrix.conjTranspose_zero

deleted theorem Matrix.conjTranspose_zsmul

deleted theorem Matrix.diag_conjTranspose

deleted theorem Matrix.diagonal_conjTranspose

deleted theorem Matrix.dotProduct_star

deleted theorem Matrix.mulVec_conjTranspose

deleted theorem Matrix.star_apply

deleted theorem Matrix.star_dotProduct

deleted theorem Matrix.star_dotProduct_star

deleted theorem Matrix.star_eq_conjTranspose

deleted theorem Matrix.star_mul

deleted theorem Matrix.star_mulVec

deleted theorem Matrix.star_vecMul

deleted theorem Matrix.vecMul_conjTranspose

Modified Mathlib/Data/Matrix/Block.lean

Created Mathlib/Data/Matrix/ConjTranspose.lean

added def Matrix.conjTranspose

added def Matrix.conjTransposeAddEquiv

added theorem Matrix.conjTransposeAddEquiv_symm

added def Matrix.conjTransposeLinearEquiv

added theorem Matrix.conjTransposeLinearEquiv_symm

added def Matrix.conjTransposeRingEquiv

added theorem Matrix.conjTranspose_add

added theorem Matrix.conjTranspose_apply

added theorem Matrix.conjTranspose_conjTranspose

added theorem Matrix.conjTranspose_eq_diagonal

added theorem Matrix.conjTranspose_eq_intCast

added theorem Matrix.conjTranspose_eq_natCast

added theorem Matrix.conjTranspose_eq_ofNat

added theorem Matrix.conjTranspose_eq_one

added theorem Matrix.conjTranspose_eq_transpose_of_trivial

added theorem Matrix.conjTranspose_eq_zero

added theorem Matrix.conjTranspose_inj

added theorem Matrix.conjTranspose_injective

added theorem Matrix.conjTranspose_intCast

added theorem Matrix.conjTranspose_intCast_smul

added theorem Matrix.conjTranspose_inv_intCast_smul

added theorem Matrix.conjTranspose_inv_natCast_smul

added theorem Matrix.conjTranspose_inv_ofNat_smul

added theorem Matrix.conjTranspose_list_prod

added theorem Matrix.conjTranspose_list_sum

added theorem Matrix.conjTranspose_map

added theorem Matrix.conjTranspose_mul

added theorem Matrix.conjTranspose_multiset_sum

added theorem Matrix.conjTranspose_natCast

added theorem Matrix.conjTranspose_natCast_smul

added theorem Matrix.conjTranspose_neg

added theorem Matrix.conjTranspose_nsmul

added theorem Matrix.conjTranspose_ofNat

added theorem Matrix.conjTranspose_ofNat_smul

added theorem Matrix.conjTranspose_one

added theorem Matrix.conjTranspose_pow

added theorem Matrix.conjTranspose_ratCast_smul

added theorem Matrix.conjTranspose_rat_smul

added theorem Matrix.conjTranspose_reindex

added theorem Matrix.conjTranspose_smul

added theorem Matrix.conjTranspose_smul_non_comm

added theorem Matrix.conjTranspose_smul_self

added theorem Matrix.conjTranspose_sub

added theorem Matrix.conjTranspose_submatrix

added theorem Matrix.conjTranspose_sum

added theorem Matrix.conjTranspose_zero

added theorem Matrix.conjTranspose_zsmul

added theorem Matrix.diag_conjTranspose

added theorem Matrix.diagonal_conjTranspose

added theorem Matrix.dotProduct_star

added theorem Matrix.mulVec_conjTranspose

added theorem Matrix.star_apply

added theorem Matrix.star_dotProduct

added theorem Matrix.star_dotProduct_star

added theorem Matrix.star_eq_conjTranspose

added theorem Matrix.star_mul

added theorem Matrix.star_mulVec

added theorem Matrix.star_vecMul

added theorem Matrix.vecMul_conjTranspose

Modified Mathlib/Data/Matrix/Invertible.lean

Modified Mathlib/Data/Matrix/RowCol.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

Modified MathlibTest/apply_fun.lean