Documentation Verification Report

EquationalCriterion

📁 Source: Mathlib/RingTheory/Flat/EquationalCriterion.lean

Statistics

Metric	Count
Definitions `IsTrivialRelation`	1
Theorems `isTrivialRelation_comp`, `exists_factorization_of_apply_eq_zero_of_free`, `exists_factorization_of_comp_eq_zero_of_free`, `exists_factorization_of_isFinitelyPresented`, `iff_forall_exists_factorization`, `iff_forall_isTrivialRelation`, `isTrivialRelation_of_sum_smul_eq_zero`, `of_forall_exists_factorization`, `of_forall_isTrivialRelation`, `projective_of_finitePresentation`, `tfae_equational_criterion`, `isTrivialRelation_iff_vanishesTrivially`, `sum_smul_eq_zero_of_isTrivialRelation`	13
Total	14

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTrivialRelation_comp` 📖	mathematical	—	`Module.IsTrivialRelation` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`vanishesTrivially_comp`

Module

Definitions

Name	Category	Theorems
`IsTrivialRelation` 📖	MathDef	4 math math: `isTrivialRelation_iff_vanishesTrivially`, `Flat.isTrivialRelation_of_sum_smul_eq_zero`, `Flat.iff_forall_isTrivialRelation`, `Equiv.isTrivialRelation_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTrivialRelation_iff_vanishesTrivially` 📖	mathematical	—	`IsTrivialRelation` `TensorProduct.VanishesTrivially` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Finset.sum_congr` `mul_comm`
`sum_smul_eq_zero_of_isTrivialRelation` 📖	mathematical	`IsTrivialRelation`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomInvPair.ids` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially` `isTrivialRelation_iff_vanishesTrivially`

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_factorization_of_apply_eq_zero_of_free` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`LinearMap.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHomCompTriple.ids` `Finsupp.instZero`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `iff_forall_exists_factorization` `LinearEquiv.apply_symm_apply` `LinearMap.comp_assoc` `LinearEquiv.eq_comp_toLinearMap_symm`
`exists_factorization_of_comp_eq_zero_of_free` 📖	mathematical	`LinearMap.comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearMap` `LinearMap.instZero`	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearMap.ext` `LinearMap.comp.congr_simp` `LinearEquiv.comp_symm_assoc` `LinearMap.comp_assoc` `LinearEquiv.eq_comp_toLinearMap_symm`
`exists_factorization_of_isFinitelyPresented` 📖	mathematical	—	`LinearMap.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Module.FinitePresentation.exists_fin` `LinearMap.comp.congr_simp` `Function.Exact.linearMap_comp_eq_zero` `LinearMap.exact_subtype_mkQ` `LinearMap.comp_zero` `exists_factorization_of_comp_eq_zero_of_free` `Module.Finite.of_fg` `Module.Free.function` `Finite.of_fintype` `Module.Free.self` `Module.Finite.pi` `Module.Finite.self` `RingHomSurjective.ids` `Submodule.range_subtype` `LinearMap.range_le_ker_iff` `LinearMap.cancel_right` `LinearEquiv.surjective` `Submodule.mkQ_surjective` `LinearEquiv.symm_trans_self` `Submodule.liftQ_mkQ`
`iff_forall_exists_factorization` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommSemiring.toSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `Finsupp.instZero`	—	`List.TFAE.out` `RingHomCompTriple.ids` `tfae_equational_criterion`
`iff_forall_isTrivialRelation` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.IsTrivialRelation` `Fin.fintype`	—	`List.TFAE.out` `RingHomCompTriple.ids` `tfae_equational_criterion`
`isTrivialRelation_of_sum_smul_eq_zero` 📖	mathematical	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Module.IsTrivialRelation`	—	`Equiv.isTrivialRelation_comp` `iff_forall_isTrivialRelation` `Equiv.sum_comp`
`of_forall_exists_factorization` 📖	mathematical	`LinearMap.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `Finsupp.instZero`	`Module.Flat`	—	`RingHomCompTriple.ids` `iff_forall_exists_factorization`
`of_forall_isTrivialRelation` 📖	mathematical	`Module.IsTrivialRelation` `Fin.fintype`	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`iff_forall_isTrivialRelation`
`projective_of_finitePresentation` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`RingHomCompTriple.ids` `exists_factorization_of_isFinitelyPresented` `Module.Projective.of_split` `Module.Projective.of_free` `Module.Free.finsupp` `Module.Free.self`
`tfae_equational_criterion` 📖	mathematical	—	`List.TFAE` `Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`iff_rTensor_injective'` `TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective` `RingHomInvPair.ids` `LinearEquiv.injective` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `RingHomCompTriple.ids` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finsupp.smul_single` `mul_one` `Finsupp.univ_sum_single` `Finite.of_fintype` `Module.Basis.ext` `Finsupp.coe_basisSingleOne` `Finsupp.sum_fintype` `zero_smul` `Finsupp.single_apply` `ite_smul` `one_smul` `Finset.sum_ite_eq` `Finsupp.ext` `Finsupp.finset_sum_apply` `Finsupp.linearCombination_single` `LinearMap.congr_fun` `DFunLike.congr_fun` `List.tfae_of_cycle`

---

← Back to Index