Commit 2025-03-05 15:27 0ae30b68

View on Github →

chore(RingTheory): merge Finiteness/TensorProduct.lean into TensorProduct/Finite.lean (#22595) These two files cover basically the same material and seem to have ended up in different locations due to historical accident. If we merge them it doesn't seem that we actually lose anything, import-wise.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Modified Mathlib/Algebra/Module/FinitePresentation.lean

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

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Charpoly/BaseChange.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Deleted Mathlib/RingTheory/Finiteness/TensorProduct.lean

deleted theorem Module.exists_isPrincipal_quotient_of_finite

deleted theorem Module.exists_surjective_quotient_of_finite

deleted theorem Submodule.exists_fg_le_eq_rTensor_inclusion

deleted theorem Submodule.exists_fg_le_eq_rTensor_subtype

deleted theorem Submodule.exists_fg_le_subset_range_rTensor_inclusion

deleted theorem Submodule.exists_fg_le_subset_range_rTensor_subtype

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Index.lean

Modified Mathlib/RingTheory/RingHom/Finite.lean

Modified Mathlib/RingTheory/TensorProduct/Finite.lean

added theorem Module.exists_isPrincipal_quotient_of_finite

added theorem Module.exists_surjective_quotient_of_finite

added theorem Submodule.exists_fg_le_eq_rTensor_inclusion

added theorem Submodule.exists_fg_le_eq_rTensor_subtype

added theorem Submodule.exists_fg_le_subset_range_rTensor_inclusion

added theorem Submodule.exists_fg_le_subset_range_rTensor_subtype