Commit 2025-02-17 00:07 4fc7e081

View on Github →

chore(LinearAlgebra): process a first batch of porting notes (#21810)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Dual.lean

modified theorem LinearMap.dualMap_def

modified theorem Module.Dual.transpose_apply

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

Modified Mathlib/LinearAlgebra/Finsupp/SumProd.lean

Modified Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/Norm.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/InvariantBasisNumber.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

Modified Mathlib/LinearAlgebra/StdBasis.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean