Documentation Verification Report

Prime

📁 Source: Mathlib/Tactic/NormNum/Prime.lean

Statistics

Metric	Count
Definitions `MinFacHelper`, `deriveNotPrime`, `evalMinFac`, `evalNatPrime`, `Prime`, `Prime`	6
Theorems `one_lt`, `isNat_minFac_1`, `isNat_minFac_2`, `isNat_minFac_3`, `isNat_minFac_4`, `isNat_not_prime`, `isNat_prime_0`, `isNat_prime_1`, `isNat_prime_2`, `minFacHelper_0`, `minFacHelper_1`, `minFacHelper_2`, `minFacHelper_3`, `not_prime_mul_of_ble`	14
Total	20

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
`MinFacHelper` 📖	MathDef	1 math math: `minFacHelper_0`
`deriveNotPrime` 📖	CompOp	—
`evalMinFac` 📖	CompOp	—
`evalNatPrime` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNat_minFac_1` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`Nat.minFac`	—	`Nat.minFac_one`
`isNat_minFac_2` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`Nat.minFac`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_ofNat` `Nat.minFac_eq_two_iff`
`isNat_minFac_3` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne` `MinFacHelper`	`Nat.minFac`	—	`le_antisymm` `Nat.minFac_le_of_dvd` `LT.lt.le`
`isNat_minFac_4` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne` `MinFacHelper`	`Nat.minFac`	—	`Nat.prime_def_minFac` `Nat.prime_def_le_sqrt` `MinFacHelper.one_lt` `lt_irrefl` `Nat.sqrt_lt` `ble_eq_false` `Nat.minFac_le_of_dvd`
`isNat_not_prime` 📖	—	`IsNat` `Nat.instAddMonoidWithOne` `Nat.Prime`	—	—	`isNat.natElim`
`isNat_prime_0` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`Nat.Prime`	—	`Nat.not_prime_zero`
`isNat_prime_1` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`Nat.Prime`	—	`Nat.not_prime_one`
`isNat_prime_2` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne` `Nat.minFac`	`Nat.Prime`	—	`Nat.prime_def_minFac`
`minFacHelper_0` 📖	mathematical	—	`MinFacHelper`	—	`Nat.le_minFac'` `LE.le.eq_or_lt`
`minFacHelper_1` 📖	—	`MinFacHelper`	—	—	`add_zero` `LE.le.eq_or_lt` `LT.lt.ne` `LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `Nat.instCharZero` `Nat.dvd_prime` `Nat.minFac_prime` `LT.lt.ne'` `MinFacHelper.one_lt`
`minFacHelper_2` 📖	—	`Nat.Prime` `MinFacHelper`	—	—	`minFacHelper_1` `Nat.minFac_prime` `LT.lt.ne'` `MinFacHelper.one_lt`
`minFacHelper_3` 📖	—	`MinFacHelper`	—	—	`minFacHelper_1` `Nat.minFac_dvd`
`not_prime_mul_of_ble` 📖	mathematical	—	`Nat.Prime`	—	`Nat.not_prime_of_mul_eq` `LT.lt.ne'` `ble_eq_false`

Mathlib.Meta.NormNum.MinFacHelper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt` 📖	—	`Mathlib.Meta.NormNum.MinFacHelper`	—	—	`LT.lt.trans_le` `LE.le.eq_or_lt` `zero_add` `Nat.minFac_one` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

PosNum

Definitions

Name	Category	Theorems
`Prime` 📖	MathDef	—

(root)

Definitions

Name	Category	Theorems
`Prime` 📖	MathDef	77 math math: `minpoly.prime_of_isIntegrallyClosed`, `IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow`, `UniqueFactorizationMonoid.mem_normalizedFactors_iff`, `Ideal.prime_of_mem_primesOver`, `PowerSeries.X_prime`, `UniqueFactorizationMonoid.exists_prime_factors`, `Nat.prime_iff_prime_int`, `Ideal.isPrime_iff_bot_or_prime`, `Polynomial.prime_C_iff`, `MvPolynomial.prime_rename_iff`, `IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two`, `prime_mul_iff`, `Nat.prime_iff`, `Polynomial.Monic.prime_of_degree_eq_one`, `MvPolynomial.X_prime`, `Int.prime_two`, `Ideal.prime_span_singleton_iff`, `Ideal.prime_of_irreducible_absNorm_span`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `not_prime_zero`, `UniqueFactorizationMonoid.exists_prime_iff`, `UniqueFactorizationMonoid.irreducible_iff_prime`, `isPrimePow_iff_pow_succ`, `prime_pow_iff`, `Int.prime_three`, `MulEquiv.prime_iff`, `Nat.irreducible_iff_prime`, `Nat.Prime.prime`, `IsSquare.not_prime`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two'`, `Nat.Primes.prodNatEquiv_apply`, `Irreducible.prime_of_isPrimal`, `Polynomial.prime_of_degree_eq_one`, `minpoly.prime`, `IsDedekindDomain.HeightOneSpectrum.prime`, `Cardinal.is_prime_iff`, `Polynomial.prime_X_sub_C`, `IsDiscreteValuationRing.exists_prime`, `MvPolynomial.prime_C_iff`, `Int.prime_ofNat_iff`, `UniqueFactorizationMonoid.prime_of_normalized_factor`, `UniqueFactorizationMonoid.prime_of_factor`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two`, `Associates.prime_mk`, `UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime`, `irreducible_iff_prime_of_existsUnique_irreducible_factors`, `Int.exists_prime_and_dvd`, `Ideal.prime_iff_isPrime`, `Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors`, `UniqueFactorizationMonoid.iff_exists_prime_factors`, `Cardinal.nat_is_prime_iff`, `Submodule.IsPrincipal.prime_generator_of_isPrime`, `Associates.exists_prime_dvd_of_not_inf_one`, `Cardinal.prime_of_aleph0_le`, `Associates.irreducible_iff_prime_iff`, `Ideal.isPrime_iff_of_isPrincipalIdealRing`, `Ideal.IsPrime.exists_mem_prime_of_ne_bot`, `Associated.prime_iff`, `isPrimePow_def`, `GaussianInt.prime_of_nat_prime_of_mod_four_eq_three`, `not_prime_one`, `not_prime_pow`, `Polynomial.prime_X`, `Irreducible.prime`, `Ideal.span_singleton_prime`, `Int.prime_iff_natAbs_prime`, `IsPrimitiveRoot.zeta_sub_one_prime`, `map_prime_of_factor_orderIso`, `irreducible_iff_prime`, `Associates.coprime_iff_inf_one`, `associates_irreducible_iff_prime`, `UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors`, `Ideal.prime_of_isPrime`, `PadicInt.prime_p`, `GaussianInt.prime_iff_mod_four_eq_three_of_nat_prime`, `IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime`, `IsPrimitiveRoot.zeta_sub_one_prime'`

---

← Back to Index