factorization_ceilRoot — Mathlib

English

The factorization of ceilRoot n a equals a.factorization ⌈/⌉ n; i.e., the exponents in the prime factorization are ceiled-divided by n.

Русский

Факторизация ceilRoot n a равна факторизации a, деленной по степеням на n с округлением вверх.

LaTeX

$$$ (\operatorname{ceilRoot}(n,a)).factorization = a.factorization \lceil/\rceil n $$$

Lean4

@[simp]
theorem factorization_ceilRoot (n a : ℕ) : (ceilRoot n a).factorization = a.factorization ⌈/⌉ n :=
  by
  rw [ceilRoot_def]
  split_ifs with h
  · obtain rfl | rfl := h <;> simp
  refine prod_pow_factorization_eq_self fun p hp ↦ ?_
  have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp
  exact this.1

Похожие утверждения