Free

📁 Source: Mathlib/Algebra/Module/Torsion/Free.lean

Statistics

Metric	Count
Definitions Free, IsTorsionFree	2
Theorems of_isAddTorsionFree, moduleIsTorsionFree, of_isDomain_charZero, of_isTorsionFree, to_isTorsionFree_nat, isSMulRegular, smul_eq_zero_iff_right, smul_ne_zero_iff_right, smul_right_inj, smul_right_injective, of_ne_zero, comap, isSMulRegular, of_smul_eq_zero, trans, isTorsionFree_iff_smul_eq_zero, isTorsionFree_int_iff_isAddTorsionFree, isTorsionFree_nat_iff_isAddTorsionFree, to_moduleIsTorsionFree, instIsTorsionFree, instIsTorsionFreeIntOfIsAddTorsionFree, instIsTorsionFreeMulOpposite, smul_eq_zero, smul_eq_zero_iff_left, smul_eq_zero_iff_right, smul_left_inj, smul_left_injective, smul_ne_zero, smul_ne_zero_iff, smul_ne_zero_iff_left, smul_ne_zero_iff_right, smul_right_inj, smul_right_injective	33
Total	35

CharZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isAddTorsionFree 📖	mathematical	—	CharZero AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	exists_ne natCast_zsmul Nat.cast_smul_eq_nsmul Int.instCharZero smul_left_injective Int.instIsCancelMulZero instIsTorsionFreeIntOfIsAddTorsionFree

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moduleIsTorsionFree 📖	mathematical	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Module.IsTorsionFree	—	IsRegular.isSMulRegular

IsAddTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isDomain_charZero 📖	mathematical	—	IsAddTorsionFree AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	of_isTorsionFree instIsTorsionFree
of_isTorsionFree 📖	mathematical	—	IsAddTorsionFree AddCommMonoid.toAddMonoid	—	Nat.cast_smul_eq_nsmul smul_right_injective
to_isTorsionFree_nat 📖	mathematical	—	Module.IsTorsionFree Nat.instSemiring AddCommMonoid.toNatModule	—	nsmul_right_injective Nat.instIsCancelMulZero Nat.instNontrivial

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSMulRegular 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Module.IsTorsionFree.isSMulRegular
smul_eq_zero_iff_right 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_zero
smul_ne_zero_iff_right 📖	—	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—	Iff.ne smul_eq_zero_iff_right
smul_right_inj 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_right_injective
smul_right_injective 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	isSMulRegular

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_ne_zero 📖	mathematical	—	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsRegular.isSMulRegular IsRegular.of_ne_zero

Module

Definitions

Name	Category	Theorems
Free 📖	CompData	85 math math: Free.finsupp, Polynomial.degreeLT.instFreeSubtypeMemSubmodule, Polynomial.Monic.free_quotient, free_iff_set, Relations.Solution.IsPresentation.free, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Subalgebra.LinearDisjoint.sup_free_of_free, Invertible.free_iff_linearEquiv, free_of_flat_of_finrank_eq, LocallyConstant.freeOfProfinite, Quaternion.instFree, exteriorPower.instFree, FreeAlgebra.instFree, CommRing.Pic.instFreeOfSubsingleton, MvPolynomial.instFree, FinitePresentation.equiv_quotient, QuadraticAlgebra.instFree, SymmetricAlgebra.instModuleFree, Free.addMonoidHom, MulOpposite.instFree, free_iff_exists_presentation, MonoidAlgebra.instFree, QuaternionAlgebra.instFree, CommRing.Pic.subsingleton_iff, TensorAlgebra.instModuleFree, Free.prod, dual_free, Free.Module.free_shrink, Free.of_subsingleton', CommRing.Pic.instFreeAsModuleOfNat, Free.linearMap, Free.of_det_ne_one, FinitePresentation.exists_free_localizedModule_powers, Algebra.TensorProduct.instFree, free_of_finite_type_torsion_free', ZLattice.module_free, SkewMonoidAlgebra.instFree, Free.tensor, free_of_isLocalizedModule, free_of_finite_type_torsion_free, free_of_maximalIdeal_rTensor_injective, mem_freeLocus_iff_tensor, Free.of_equiv', LinearMap.free_of_det_ne_one, NumberField.RingOfIntegers.instFreeInt, Submodule.IsLattice.free, Profinite.NobelingProof.Nobeling_aux, Free.of_basis, Free.of_subsingleton, IsBaseChange.free, Algebra.SubmersivePresentation.free_kaehlerDifferential, ModuleCat.free_shortExact, Free.matrix, CommRing.Pic.mk_eq_one_iff_free, Free.of_ringEquiv, Free.of_equiv, Polynomial.instFree, free_def, Free.self, Free.of_divisionRing, AddMonoidAlgebra.instFree, Free.trans, Algebra.IsStandardSmooth.free_kaehlerDifferential, mem_freeLocus_of_isLocalization, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree, FreeAbelianGroup.instFreeInt, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.SubmersivePresentation.free_cotangent, mem_freeLocus, Representation.free_asModule_free, Free.iff_of_ringEquiv, Algebra.instFreeCotangentToExtensionUnitLocalizationAway, Polynomial.Monic.free_adjoinRoot, instModuleFree_of_discrete_submodule, IsIntegralClosure.module_free, Free.ulift, instFreeCarrierX₂ModuleCatProjectiveShortComplex, free_of_flat_of_isLocalRing, Algebra.IsQuadraticExtension.toFree, instFreeMvPolynomialKaehlerDifferential, free_iff_isTorsionFree, Free.function, CommRing.Pic.subsingleton_iffₛ, free_of_lTensor_residueField_injective, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion
IsTorsionFree 📖	CompData	66 math math: isTorsionFree_int_iff_isAddTorsionFree, LinearMap.instIsTorsionFree, Ring.instIsTorsionFreeNormalClosure, instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing, NumberField.RingOfIntegers.instIsTorsionFree_1, Subalgebra.instIsTorsionFree', instIsTorsionFree, instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors, AlternatingMap.instIsTorsionFree, Prod.moduleIsTorsionFree, NoZeroSMulDivisors.iff_faithfulSMul, AddMonoidAlgebra.instIsTorsionFree, NumberField.RingOfIntegers.instIsTorsionFree_2, Subalgebra.instIsTorsionFree, QuaternionAlgebra.instIsTorsionFree, IsTorsionFree.of_faithfulSMul, LieSubmodule.instIsTorsionFreeSubtypeMem, NonUnitalStarSubalgebra.instIsTorsionFree, IsLocalizedModule.isTorsionFree, isTorsionFree_nat_iff_isAddTorsionFree, IsReflexive.to_isTorsionFree, CyclotomicRing.instIsTorsionFreeOfIsDomainOfIsFractionRing, instIsTorsionFreeMulOpposite, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Basis.isTorsionFree, IsTorsionFree.comap, IsIntegralClosure.isTorsionFree, Subsingleton.to_moduleIsTorsionFree, Polynomial.IsSplittingField.instIsTorsionFreeSplittingField, Ideal.instIsTorsionFreeSubtypeMemSubmodule, isTorsionFree_iff_algebraMap_injective, MultilinearMap.instIsTorsionFree, NumberField.RingOfIntegers.instIsTorsionFree, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, Polynomial.instIsTorsionFree, NoZeroSMulDivisors.iff_algebraMap_injective, Valuation.HasExtension.instIsTorsionFreeInteger, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, isTorsionFree_iff_faithfulSMul, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, Submodule.QuotientTorsion.instIsTorsionFree, AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero, IsLocalizedModule.isTorsionFree_of_forall_isRegular, isTorsionFree_iff_smul_eq_zero, NonUnitalSubalgebra.instIsTorsionFree, Submodule.instIsTorsionFree, IsTorsionFree.trans, IsTorsionFree.of_isLocalization, DivisionSemiring.to_moduleIsTorsionFree, MonoidAlgebra.instIsTorsionFree, Submodule.isTorsionFree_iff_torsion_eq_bot, CyclotomicRing.instIsTorsionFreeCyclotomicField, Function.Injective.moduleIsTorsionFree, QuadraticAlgebra.instIsTorsionFree, Finsupp.moduleIsTorsionFree, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, IsTorsionFree.trans_faithfulSMul, HahnModule.instIsTorsionFree, IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain, instIsTorsionFreeIntOfIsAddTorsionFree, free_iff_isTorsionFree, Free.instIsTorsionFree, MeasureTheory.Measure.instModuleIsTorsionFree, IsTorsionFree.of_smul_eq_zero, IsAddTorsionFree.to_isTorsionFree_nat, FaithfulSMul.to_isTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTorsionFree_iff_smul_eq_zero 📖	mathematical	—	IsTorsionFree Ring.toSemiring AddCommGroup.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	smul_eq_zero IsDomain.toIsCancelMulZero IsTorsionFree.of_smul_eq_zero IsDomain.toNontrivial
isTorsionFree_int_iff_isAddTorsionFree 📖	mathematical	—	IsTorsionFree Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule IsAddTorsionFree SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	IsAddTorsionFree.of_isTorsionFree Int.instIsCancelMulZero Int.instCharZero instIsTorsionFreeIntOfIsAddTorsionFree
isTorsionFree_nat_iff_isAddTorsionFree 📖	mathematical	—	IsTorsionFree Nat.instSemiring AddCommMonoid.toNatModule IsAddTorsionFree AddCommMonoid.toAddMonoid	—	IsAddTorsionFree.of_isTorsionFree Nat.instIsCancelMulZero Nat.instCharZero IsAddTorsionFree.to_isTorsionFree_nat

Module.IsTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Module.IsTorsionFree	—	IsSMulRegular.of_map IsRegular.isSMulRegular
isSMulRegular 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
of_smul_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Module.IsTorsionFree Ring.toSemiring AddCommGroup.toAddCommMonoid	—	IsRegular.ne_zero smul_sub
trans 📖	mathematical	—	Module.IsTorsionFree	—	IsRegular.isSMulRegular smul_one_mul mul_smul_one smul_assoc one_smul

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_moduleIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree	—	Function.injective_of_subsingleton

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsRegular.left
instIsTorsionFreeIntOfIsAddTorsionFree 📖	mathematical	—	Module.IsTorsionFree Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule	—	zsmul_right_injective Int.instIsCancelMulZero Int.instNontrivial
instIsTorsionFreeMulOpposite 📖	mathematical	—	Module.IsTorsionFree MulOpposite MulOpposite.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toOppositeModule	—	IsRegular.right IsRegular.unop
smul_eq_zero 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eq_or_ne zero_smul
smul_eq_zero_iff_left 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
smul_eq_zero_iff_right 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsRegular.smul_eq_zero_iff_right IsRegular.of_ne_zero
smul_left_inj 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	smul_left_injective
smul_left_injective 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	sub_eq_zero smul_eq_zero_iff_left sub_smul
smul_ne_zero 📖	—	—	—	—	—
smul_ne_zero_iff 📖	—	—	—	—	—
smul_ne_zero_iff_left 📖	—	—	—	—	—
smul_ne_zero_iff_right 📖	—	—	—	—	Iff.ne smul_eq_zero_iff_right
smul_right_inj 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsRegular.of_ne_zero
smul_right_injective 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsRegular.smul_right_injective IsRegular.of_ne_zero

---

← Back to Index