Commit 2025-01-10 18:59 f8adbb93

View on Github →

chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) Remove exists_factorization_of_apply_eq_zero as it's a special case of exists_factorization_of_apply_eq_zero_of_free. Remove one statement from the TFAE, but still keep the forward direction exists_factorization_of_apply_eq_zero_of_free` and make it fully universe polymorphic.

Estimated changes

Modified Mathlib/Algebra/Module/FinitePresentation.lean

modified theorem Module.FinitePresentation.equiv_quotient

added theorem Module.FinitePresentation.exists_fin

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

added theorem Equiv.vanishesTrivially_comp

added theorem TensorProduct.VanishesTrivially.of_fintype

deleted theorem TensorProduct.forall_vanishesTrivially_iff_forall_FG_rTensor_injective

added theorem TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective

deleted theorem TensorProduct.rTensor_injective_of_forall_FG_rTensor_injective

added theorem TensorProduct.rTensor_injective_of_forall_fg_rTensor_injective

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

added theorem Equiv.isTrivialRelation_comp

deleted theorem Module.Flat.exists_factorization_of_apply_eq_zero

modified theorem Module.Flat.exists_factorization_of_apply_eq_zero_of_free

modified theorem Module.Flat.exists_factorization_of_comp_eq_zero_of_free

modified theorem Module.Flat.exists_factorization_of_isFinitelyPresented

modified theorem Module.Flat.iff_forall_isTrivialRelation

modified theorem Module.Flat.isTrivialRelation_of_sum_smul_eq_zero

modified theorem Module.Flat.of_forall_exists_factorization

modified theorem Module.Flat.of_forall_isTrivialRelation

added theorem Module.Flat.projective_of_finitePresentation