Commit 2026-06-18 10:07 7c0bf438

View on Github →

feat(LinearAlgebra): generators of pi tensor products (#26464) In this PR, we show that the R-module ⨂[R] i, M i is finitely generated if the index type is finite and all M i are finitely generated. This follows from a more precise result about generators of ⨂[R] i, M i.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Set.ncard_compl_add_ncard

added theorem Set.ncard_compl_of_ncard_eq_add

Created Mathlib/Data/SubtypeNeLift.lean

added def Function.subtypeNeLift

added theorem Function.subtypeNeLift_of_neq

added theorem Function.subtypeNeLift_restriction

added theorem Function.subtypeNeLift_self

Renamed Mathlib/LinearAlgebra/PiTensorProduct.lean to Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct/DirectSum.lean

Created Mathlib/LinearAlgebra/PiTensorProduct/Finite.lean

Created Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean

added theorem MultilinearMap.ext_of_span_eq_top

added theorem PiTensorProduct.equivPiTensorComplSingletonTensor_symm_tmul

added theorem PiTensorProduct.equivPiTensorComplSingletonTensor_tprod

added theorem PiTensorProduct.ext_of_span_eq_top

added theorem PiTensorProduct.submodule_span_eq_top

Modified Mathlib/LinearAlgebra/TensorPower/Basic.lean

Modified Mathlib/LinearAlgebra/TensorPower/Symmetric.lean

Modified Mathlib/Logic/Equiv/Option.lean

Modified Mathlib/RingTheory/PiTensorProduct.lean