No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
38@[simp] theorem prime_iff (n : ℕ) : Prime n ↔ Nat.Prime n := Iff.rfl
proof body
Term-mode proof.
39
40end Primes
41end NumberTheory
42end IndisputableMonolith
used by (36)
From the project-wide theorem graph. These declarations reference this one in their body.
-
bigOmega_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
bigOmega_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
coprime_pow_of_prime_not_dvd
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
coprime_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
divisors_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
liouville_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
liouville_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
mobius_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
mobius_prime_sq
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
omega_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
omega_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
primeFactors_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
primeFactors_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
radical_prime'
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
sigma_one_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
sigma_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
sigma_zero_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
sigma_zero_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
totient_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
totient_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
vonMangoldt_prime
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
vonMangoldt_prime_pow
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
pow_dvd_iff_le_vp
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
prime_dvd_iff_vp_pos
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
vp_prime_ne
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
vp_prime_pow
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
vp_prime_pow_ne
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
vp_prime_self
in IndisputableMonolith.NumberTheory.Primes.Factorization
decl_use
-
prime_dvd_wheel840
in IndisputableMonolith.NumberTheory.Primes.Modular
decl_use
-
squarefree_iff_vp_le_one_of_prime
in IndisputableMonolith.NumberTheory.Primes.Squarefree
decl_use
… and 6 more
depends on (2)
Lean names referenced from this declaration's body.
-
Primes
in IndisputableMonolith.NumberTheory.EulerInstantiation
decl_use
-
Prime
in IndisputableMonolith.NumberTheory.Primes.Basic
decl_use