Theorems · Definition · number theory

Nat.ceilRoot

ℕ → ℕ → ℕ

Ceiling root of a natural number. This divides the valuation of every prime number rounding up. Eg if n = 3, a = 2^4 * 3^2 * 5, then ceilRoot n a = 2^2 * 3 * 5. In order theory terms, this is the lower or left adjoint of the map a ↦ a ^ n : ℕ → ℕ where ℕ is ordered by divisibility. To ensure that the adjunction (Nat.dvd_pow_iff_ceilRoot_dvd) holds in as many cases as possible, we special-case the following values: * ceilRoot 0 a = 0 (this one is not strictly necessary) * ceilRoot n 0 = 0

Defined in

Mathlib.Data.Nat.Factorization.Root

Cited by

11 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound