Documentation Verification Report

NoZeroDivisors

📁 Source: Mathlib/RingTheory/PowerSeries/NoZeroDivisors.lean

Statistics

Metric	Count
Definitions `NoZeroDivisors`	1
Theorems `X_irreducible`, `X_prime`, `instIsDomain`, `instNoZeroDivisors`, `rescale_injective`, `span_X_isPrime`	6
Total	7

PowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_irreducible` 📖	mathematical	—	`Irreducible` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `X`	—	`Prime.irreducible` `IsDomain.toIsCancelMulZero` `instIsDomain` `X_prime`
`X_prime` 📖	mathematical	—	`Prime` `PowerSeries` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `CommRing.toCommSemiring` `X` `CommSemiring.toSemiring`	—	`Ideal.span_singleton_prime` `coeff_one_X` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `NeZero.one` `IsDomain.toNontrivial` `span_X_isPrime`
`instIsDomain` 📖	mathematical	—	`IsDomain` `PowerSeries` `instSemiring` `Ring.toSemiring`	—	`NoZeroDivisors.to_isDomain` `instNontrivial` `IsDomain.toNontrivial` `instNoZeroDivisors` `IsDomain.to_noZeroDivisors`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `PowerSeries` `MvPowerSeries.instMul` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`WithTop.add_eq_top` `order_mul`
`rescale_injective` 📖	mathematical	—	`PowerSeries` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `rescale`	—	`ext_iff` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `coeff_rescale`
`span_X_isPrime` 📖	mathematical	—	`Ideal.IsPrime` `PowerSeries` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.span` `Set` `Set.instSingletonSet` `X`	—	`RingHom.instRingHomClass` `Ideal.ext` `RingHom.mem_ker` `Ideal.mem_span_singleton` `X_dvd_iff` `RingHom.ker_isPrime`

(root)

Definitions

Name	Category	Theorems
`NoZeroDivisors` 📖	CompData	68 math math: `HahnSeries.instNoZeroDivisorsFinsuppNat`, `Set.instNoZeroDivisors`, `Quaternion.instNoZeroDivisors`, `noZeroDivisors_iff_isDomain_or_subsingleton`, `Ordinal.noZeroDivisors`, `IsLocalization.noZeroDivisors`, `noZeroDivisors_tfae`, `IsDomain.to_noZeroDivisors`, `Tropical.instNoZeroDivisorsWithTop`, `NonUnitalSubsemiringClass.noZeroDivisors`, `Nimber.instNoZeroDivisors`, `AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums`, `instNoZeroDivisorsOrderDual`, `WittVector.instNoZeroDivisorsOfCharP`, `Zsqrtd.instNoZeroDivisorsCastInt`, `Submonoid.LocalizationMap.noZeroDivisors`, `WithZero.instNoZeroDivisors`, `SubsemiringClass.noZeroDivisors`, `Subsemiring.noZeroDivisors`, `Polynomial.noZeroDivisors_iff`, `NonUnitalSubalgebra.noZeroDivisors`, `TensorAlgebra.instNoZeroDivisors`, `Localization.instNoZeroDivisors`, `Subsingleton.to_noZeroDivisors`, `FreeAlgebra.instNoZeroDivisors`, `HahnSeries.instNoZeroDivisors`, `Finset.instNoZeroDivisors`, `noZeroDivisors_iff_left_eq_zero_of_mul`, `noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight`, `MvPolynomial.instNoZeroDivisors`, `Subalgebra.noZeroDivisors`, `IsStrictOrderedRing.noZeroDivisors`, `noZeroDivisors_iff_forall_mem_nonZeroDivisors`, `Associates.instNoZeroDivisors`, `MonoidAlgebra.instNoZeroDivisorsOfUniqueProds`, `PowerSeries.instNoZeroDivisors`, `NoZeroDivisors.of_faithfulSMul`, `MulEquiv.noZeroDivisors_iff`, `WithBot.instNoZeroDivisors`, `EReal.instNoZeroDivisors`, `Polynomial.instNoZeroDivisors`, `Cardinal.noZeroDivisors`, `NonUnitalStarSubalgebra.instNoZeroDivisors`, `instNoZeroDivisorsLex`, `Nonneg.noZeroDivisors`, `MulOpposite.instNoZeroDivisors`, `Subring.instNoZeroDivisorsSubtypeMem`, `NormMulClass.toNoZeroDivisors`, `isDomain_iff_noZeroDivisors_and_nontrivial`, `Ideal.instNoZeroDivisors`, `IsLeftCancelMulZero.to_noZeroDivisors`, `MvPowerSeries.instNoZeroDivisors`, `noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft`, `noZeroDivisors_iff`, `Function.Injective.noZeroDivisors`, `SymmetricAlgebra.instNoZeroDivisors`, `AddOpposite.instNoZeroDivisors`, `WithTop.instNoZeroDivisors`, `ENNReal.instNoZeroDivisors`, `SetSemiring.instNoZeroDivisors`, `MulEquiv.noZeroDivisors`, `isCancelMulZero_iff_noZeroDivisors`, `NNReal.instNoZeroDivisors`, `GroupWithZero.noZeroDivisors`, `noZeroDivisors_iff_eq_zero_of_mul`, `noZeroDivisors_iff_right_eq_zero_of_mul`, `IsRightCancelMulZero.to_noZeroDivisors`, `Ideal.Quotient.noZeroDivisors`

---

← Back to Index