factorization_floorRoot — Mathlib

English

The factorization of floorRoot(n,a) equals the floor-divided factorization of a by n.

Русский

Разложение floorRoot(n,a) по простым равно разложению a по простым с делением показателей на n.

LaTeX

$$$(\text{floorRoot}(n,a)).factorization = a.factorization ⌊/⌋ n$$$

Lean4

@[simp]
theorem factorization_floorRoot (n a : ℕ) : (floorRoot n a).factorization = a.factorization ⌊/⌋ n :=
  by
  rw [floorRoot_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_floorDiv_subset hp
  exact this.1

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