Documentation Verification Report

TorsionFree

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

Statistics

Metric	Count
Definitions	0
Theorems `flat_iff_torsion_eq_bot`, `flat_iff_torsion_eq_bot_of_isBezout`, `flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal`, `instOfIsDedekindDomainOfIsTorsionFree`, `isSMulRegular_of_isRegular`, `isSMulRegular_of_nonZeroDivisors`, `torsion_eq_bot`	7
Total	7

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat_iff_torsion_eq_bot` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.torsion` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `Submodule.instBot`	—	`Module.Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal` `toIsDomain` `Ideal.IsMaximal.isPrime'` `IsLocalization.isDomain_of_local_atPrime` `ValuationRing.instOfIsLocalRingOfIsBezout` `Localization.AtPrime.isLocalRing` `IsBezout.of_isPrincipalIdealRing` `isPrincipalIdealRing` `Localization.AtPrime.isDedekindDomain`

Module.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat_iff_torsion_eq_bot_of_isBezout` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.torsion` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `Submodule.instBot`	—	`torsion_eq_bot` `smulCommClass_self` `RingHomCompTriple.ids` `iff_lift_lsmul_comp_subtype_injective` `eq_or_ne` `Unique.instSubsingleton` `IsBezout.isPrincipal_of_FG` `Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero` `Function.Injective.of_comp_right` `RingHomInvPair.ids` `LinearEquiv.coe_toLinearMap` `LinearMap.coe_comp` `LinearEquiv.coe_rTensor` `LinearMap.rTensor.eq_1` `TensorProduct.lift_comp_map` `LinearMap.compl₂_id` `LinearMap.comp_assoc` `Algebra.to_smulCommClass` `IsScalarTower.right` `Ideal.subtype_isoBaseOfIsPrincipal_eq_mul` `LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul` `LinearMap.lsmul_injective` `Submodule.isTorsionFree_iff_torsion_eq_bot` `Equiv.injective_comp` `one_smul` `LinearEquiv.surjective`
`flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal` 📖	mathematical	`ValuationRing` `Localization` `CommRing.toCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.IsMaximal.isPrime'` `OreLocalization.instCommRing` `OreLocalization.oreSetComm` `IsLocalization.isDomain_of_local_atPrime`	`Module.Flat` `AddCommGroup.toAddCommMonoid` `Submodule.torsion` `Bot.bot` `Submodule` `Submodule.instBot`	—	`Ideal.IsMaximal.isPrime'` `IsLocalization.isDomain_of_local_atPrime` `torsion_eq_bot` `Module.flat_of_localized_maximal` `IsScalarTower.left` `IsScalarTower.right` `Module.flat_iff_of_isLocalization` `Localization.isLocalization` `OreLocalization.instIsScalarTower_1` `flat_iff_torsion_eq_bot_of_isBezout` `ValuationRing.instIsBezout` `Submodule.isTorsionFree_iff_torsion_eq_bot` `IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain`
`instOfIsDedekindDomainOfIsTorsionFree` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsDedekindDomain.flat_iff_torsion_eq_bot` `Submodule.isTorsionFree_iff_torsion_eq_bot` `IsDedekindDomain.toIsDomain`
`isSMulRegular_of_isRegular` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`rTensor_preserves_injective_linearMap` `IsRegular.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `one_mul` `IsSMulRegular.eq_1`
`isSMulRegular_of_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`isSMulRegular_of_isRegular` `le_nonZeroDivisors_iff_isRegular` `le_refl`
`torsion_eq_bot` 📖	mathematical	—	`Submodule.torsion` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `Submodule.instBot`	—	`eq_bot_iff` `isSMulRegular_of_nonZeroDivisors` `smul_zero`

---

← Back to Index