Commit 2024-11-05 12:09 426be0c2

View on Github →

chore(RingTheory/TensorProduct): split finite/free results into new files (#18653)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

Modified Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/LinearDisjoint.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/QuotSMulTop.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

deleted theorem Algebra.TensorProduct.basisAux_map_smul

deleted theorem Algebra.TensorProduct.basisAux_tmul

deleted theorem Algebra.TensorProduct.basis_apply

deleted theorem Algebra.TensorProduct.basis_repr_symm_apply'

deleted theorem Algebra.TensorProduct.basis_repr_symm_apply

deleted theorem Algebra.TensorProduct.basis_repr_tmul

deleted theorem Basis.baseChange_end

deleted theorem Basis.baseChange_linearMap

deleted theorem LinearMap.toMatrix_baseChange

deleted theorem Subalgebra.finite_sup

Created Mathlib/RingTheory/TensorProduct/Finite.lean

added theorem Subalgebra.finite_sup

Created Mathlib/RingTheory/TensorProduct/Free.lean

added theorem Algebra.TensorProduct.basisAux_map_smul

added theorem Algebra.TensorProduct.basisAux_tmul

added theorem Algebra.TensorProduct.basis_apply

added theorem Algebra.TensorProduct.basis_repr_symm_apply'

added theorem Algebra.TensorProduct.basis_repr_symm_apply

added theorem Algebra.TensorProduct.basis_repr_tmul

added theorem Basis.baseChange_end

added theorem Basis.baseChange_linearMap

added theorem LinearMap.toMatrix_baseChange