Commit 2025-04-08 10:56 386dd10a

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Dual/Defs.lean

modified def Submodule.dualAnnihilator

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

Modified Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

Modified Mathlib/LinearAlgebra/Projectivization/Subspace.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean