Commit 2024-12-19 10:05 3c80bbfb

View on Github →

chore: unnamespace Matrix.dotProduct (#19910) Moves:

Matrix.dotProduct -> dotProduct
Matrix.dotProductᵣ -> dotProductᵣ
The notation ⬝ᵥ will no longer be scoped.
Lemmas about dotProduct that don't talk about matrices will be unnamespaced accordingly Discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Matrix.2EdotProduct.20rename.3F

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Data/Matrix/Mul.lean

deleted theorem Matrix.add_dotProduct

deleted theorem Matrix.comp_equiv_dotProduct_comp_equiv

deleted theorem Matrix.comp_equiv_symm_dotProduct

deleted theorem Matrix.diagonal_dotProduct

deleted def Matrix.dotProduct

deleted theorem Matrix.dotProduct_add

deleted theorem Matrix.dotProduct_assoc

deleted theorem Matrix.dotProduct_comm

deleted theorem Matrix.dotProduct_comp_equiv_symm

deleted theorem Matrix.dotProduct_diagonal'

deleted theorem Matrix.dotProduct_diagonal

deleted theorem Matrix.dotProduct_neg

deleted theorem Matrix.dotProduct_one

deleted theorem Matrix.dotProduct_pUnit

deleted theorem Matrix.dotProduct_single

deleted theorem Matrix.dotProduct_single_one

deleted theorem Matrix.dotProduct_smul

deleted theorem Matrix.dotProduct_sub

deleted theorem Matrix.dotProduct_zero'

deleted theorem Matrix.dotProduct_zero

deleted theorem Matrix.neg_dotProduct

deleted theorem Matrix.neg_dotProduct_neg

deleted theorem Matrix.one_dotProduct

deleted theorem Matrix.one_dotProduct_one

deleted theorem Matrix.single_dotProduct

deleted theorem Matrix.single_one_dotProduct

deleted theorem Matrix.smul_dotProduct

deleted theorem Matrix.sub_dotProduct

deleted theorem Matrix.sum_elim_dotProduct_sum_elim

deleted theorem Matrix.zero_dotProduct'

deleted theorem Matrix.zero_dotProduct

added theorem add_dotProduct

added theorem comp_equiv_dotProduct_comp_equiv

added theorem comp_equiv_symm_dotProduct

added theorem diagonal_dotProduct

added def dotProduct

added theorem dotProduct_add

added theorem dotProduct_assoc

added theorem dotProduct_comm

added theorem dotProduct_comp_equiv_symm

added theorem dotProduct_diagonal'

added theorem dotProduct_diagonal

added theorem dotProduct_neg

added theorem dotProduct_one

added theorem dotProduct_pUnit

added theorem dotProduct_single

added theorem dotProduct_single_one

added theorem dotProduct_smul

added theorem dotProduct_sub

added theorem dotProduct_zero'

added theorem dotProduct_zero

added theorem neg_dotProduct

added theorem neg_dotProduct_neg

added theorem one_dotProduct

added theorem one_dotProduct_one

added theorem single_dotProduct

added theorem single_one_dotProduct

added theorem smul_dotProduct

added theorem sub_dotProduct

added theorem sum_elim_dotProduct_sum_elim

added theorem zero_dotProduct'

added theorem zero_dotProduct

Modified Mathlib/Data/Matrix/Reflection.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Matrix.lean

Modified Mathlib/LinearAlgebra/CrossProduct.lean

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

deleted theorem Matrix.dotProduct_eq

deleted theorem Matrix.dotProduct_eq_iff

deleted theorem Matrix.dotProduct_eq_zero

deleted theorem Matrix.dotProduct_eq_zero_iff

deleted theorem Matrix.dotProduct_le_dotProduct_of_nonneg_left

deleted theorem Matrix.dotProduct_le_dotProduct_of_nonneg_right

deleted theorem Matrix.dotProduct_nonneg_of_nonneg

deleted theorem Matrix.dotProduct_self_eq_zero

deleted theorem Matrix.dotProduct_self_star_eq_zero

deleted theorem Matrix.dotProduct_self_star_nonneg

deleted theorem Matrix.dotProduct_star_self_eq_zero

deleted theorem Matrix.dotProduct_star_self_nonneg

deleted theorem Matrix.dotProduct_stdBasis_eq_mul

deleted theorem Matrix.dotProduct_stdBasis_one

added theorem dotProduct_eq

added theorem dotProduct_eq_iff

added theorem dotProduct_eq_zero

added theorem dotProduct_eq_zero_iff

added theorem dotProduct_le_dotProduct_of_nonneg_left

added theorem dotProduct_le_dotProduct_of_nonneg_right

added theorem dotProduct_nonneg_of_nonneg

added theorem dotProduct_self_eq_zero

added theorem dotProduct_self_star_eq_zero

added theorem dotProduct_self_star_nonneg

added theorem dotProduct_star_self_eq_zero

added theorem dotProduct_star_self_nonneg

added theorem dotProduct_stdBasis_eq_mul

added theorem dotProduct_stdBasis_one

Modified Mathlib/LinearAlgebra/Matrix/Gershgorin.lean

Modified Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

Modified Mathlib/LinearAlgebra/Matrix/Orthogonal.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/Projectivization/Constructions.lean

Modified Mathlib/Tactic/ScopedNS.lean

Modified scripts/nolints_prime_decls.txt