Commit 2023-08-23 11:25 41eb5e6b

View on Github →

chore: remove autoImplicit in LinearAlgebra (#6634) In Mathlib/LinearAlgebra/Dual.lean we also overhaul the universe argument names, as the file switched between two conventions and making up undeclared universe variables. Mathlib/LinearAlgebra/Prod.lean invented some new variables even though it already had plenty available.

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

modified theorem AffineMap.const_apply

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/Basic.lean

modified theorem LinearEquiv.ofLinear_apply

modified theorem LinearEquiv.ofLinear_symm_apply

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Prod.lean

modified theorem LinearMap.prod_comp

Modified Mathlib/LinearAlgebra/Span.lean

modified theorem Submodule.span_induction₂

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

modified theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul