Documentation Verification Report

NatInt

📁 Source: Mathlib/RingTheory/Radical/NatInt.lean

Statistics

Metric	Count
Definitions `evalRadical`	1
Theorems `one_lt_radical_iff`, `radical_eq_one_iff`, `radical_eq_prod_primeFactors`, `radical_le_one_iff`, `radical_natAbs_eq_radical`, `radical_natCast`, `radical_pos`, `two_le_radical_iff`, `one_lt_radical_iff`, `radical_eq_one_iff`, `radical_eq_prod_primeFactors`, `radical_le_one_iff`, `radical_le_self_iff`, `radical_pos`, `self_lt_radical_iff`, `two_le_radical_iff`, `primeFactors_eq_natPrimeFactors`, `primeFactors_eq_primeFactors_natAbs`	18
Total	19

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Nat.instUniqueFactorizationMonoid` `radical_natAbs_eq_radical` `Nat.one_lt_cast` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `Nat.one_lt_radical_iff`
`radical_eq_one_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `radical_le_one_iff`
`radical_eq_prod_primeFactors` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain` `Finset.prod` `Nat.instCommMonoid` `Nat.primeFactors`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Nat.instUniqueFactorizationMonoid` `radical_natAbs_eq_radical` `Nat.radical_eq_prod_primeFactors`
`radical_le_one_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Iff.not` `one_lt_radical_iff`
`radical_natAbs_eq_radical` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `Nat.instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `Nat.instUniqueFactorizationMonoid` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`Nat.instUniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Nat.radical_eq_prod_primeFactors` `UniqueFactorizationMonoid.radical.eq_1` `Nat.cast_prod` `instCharZero` `Finset.prod_congr` `UniqueFactorizationMonoid.primeFactors_eq_primeFactors_natAbs` `Finset.prod_map`
`radical_natCast` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain` `Nat.instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `Nat.instUniqueFactorizationMonoid`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Nat.instUniqueFactorizationMonoid` `radical_eq_prod_primeFactors` `Nat.cast_prod` `Nat.radical_eq_prod_primeFactors`
`radical_pos` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Nat.instUniqueFactorizationMonoid` `radical_natAbs_eq_radical` `Nat.radical_pos`
`two_le_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instCommRing` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `euclideanDomain`	—	`one_lt_radical_iff`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`pos_of_mem_primeFactors` `instUniqueFactorizationMonoid` `radical_eq_prod_primeFactors` `nonempty_primeFactors` `Finset.one_lt_prod_iff_of_one_le` `instMulLeftMono` `Prime.one_lt` `mem_primeFactors`
`radical_eq_one_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`instUniqueFactorizationMonoid` `radical_le_one_iff`
`radical_eq_prod_primeFactors` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid` `Finset.prod` `instCommMonoid` `primeFactors`	—	`instUniqueFactorizationMonoid` `Finset.prod_congr` `UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors`
`radical_le_one_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`instUniqueFactorizationMonoid` `Iff.not` `one_lt_radical_iff`
`radical_le_self_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.radical_zero` `instCanonicallyOrderedAdd` `UniqueFactorizationMonoid.radical_dvd_self`
`radical_pos` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`pos_of_ne_zero` `instCanonicallyOrderedAdd` `instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.radical_ne_zero` `instNontrivial`
`self_lt_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`instUniqueFactorizationMonoid` `Iff.not` `radical_le_self_iff`
`two_le_radical_iff` 📖	mathematical	—	`UniqueFactorizationMonoid.radical` `instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `instUniqueFactorizationMonoid`	—	`one_lt_radical_iff`

Nat.Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalRadical` 📖	CompOp	—

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primeFactors_eq_natPrimeFactors` 📖	mathematical	—	`primeFactors` `Nat.instCommMonoidWithZero` `NormalizedGCDMonoid.toNormalizationMonoid` `instNormalizedGCDMonoidNat` `Nat.instUniqueFactorizationMonoid` `Nat.primeFactors`	—	`Nat.instUniqueFactorizationMonoid` `primeFactors.eq_1` `Unique.instSubsingleton` `Nat.factors_eq` `Nat.primeFactors.eq_1` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `List.toFinset_coe`
`primeFactors_eq_primeFactors_natAbs` 📖	mathematical	—	`primeFactors` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `Int.normalizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Int.instCommRing` `Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Int.euclideanDomain` `Finset.map` `Nat.castEmbedding` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `Int.instCharZero` `Nat.primeFactors`	—	`PrincipalIdealRing.to_uniqueFactorizationMonoid` `Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `Int.instCharZero` `eq_or_ne` `primeFactors_zero` `Nat.primeFactors_zero` `Finset.ext` `mem_primeFactors` `mem_normalizedFactors_iff'` `irreducible_iff_prime` `Int.instIsCancelMulZero` `instDecompositionMonoid` `Int.nonneg_iff_normalize_eq_self` `Finset.mem_map` `Function.Embedding.inj'` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `Nat.prime_iff_prime_int` `Int.natCast_dvd` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`

---

← Back to Index