Commit 2025-04-10 17:59 af8d2825

View on Github →

chore(LinearAlgebra): process misc porting notes (#23908)

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

modified theorem Matrix.GeneralLinearGroup.coe_toLin

modified theorem Matrix.GeneralLinearGroup.toLin_apply

Modified Mathlib/LinearAlgebra/Projectivization/Basic.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean