Commit 2025-04-03 04:39 9e808780

View on Github →

chore(LinearAlgebra/*): process misc porting notes (#23551)

Estimated changes

Modified Mathlib/Data/Matrix/Notation.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/CrossProduct.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/Orientation.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/LinearAlgebra/Ray.lean

modified theorem Module.Ray.units_smul_of_neg

modified theorem Module.Ray.units_smul_of_pos

modified theorem sameRay_of_mem_orbit

modified theorem units_smul_eq_self_iff

Modified Mathlib/LinearAlgebra/UnitaryGroup.lean