English
Re-statement: a = p^{Nat.find (fun n => a ∣ p^n) ⟨n,h⟩} when a | p^n with hp irreducible.
Русский
Повторение: если a|p^n и p ирредуцируемый, то a = p^{Nat.find …}.
LaTeX
$$$a = p^{\\operatorname{Nat.find}(\\lambda t, a \\mid p^t) \\langle n,h \\rangle}$$$
Lean4
/-- If `f` maps `p ^ i` to `(f p) ^ i` for primes `p`, and `f`
is multiplicative on coprime elements, then `f` is multiplicative everywhere. -/
theorem multiplicative_of_coprime (f : α → β) (a b : α) (h0 : f 0 = 0) (h1 : ∀ {x y}, IsUnit y → f (x * y) = f x * f y)
(hpr : ∀ {p} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y}, IsRelPrime x y → f (x * y) = f x * f y) :
f (a * b) = f a * f b := by
letI := Classical.decEq α
by_cases ha0 : a = 0
· rw [ha0, zero_mul, h0, zero_mul]
by_cases hb0 : b = 0
· rw [hb0, mul_zero, h0, mul_zero]
by_cases hf1 : f 1 = 0
·
calc
f (a * b) = f (a * b * 1) := by rw [mul_one]
_ = 0 := by simp only [h1 isUnit_one, hf1, mul_zero]
_ = f a * f (b * 1) := by simp only [h1 isUnit_one, hf1, mul_zero]
_ = f a * f b := by rw [mul_one]
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
letI : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
suffices
f
(∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
p ^ ((normalizedFactors a).count p + (normalizedFactors b).count p)) =
f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ^ (normalizedFactors a).count p) *
f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ^ (normalizedFactors b).count p)
by
obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
rw [← a_eq, ← b_eq,
mul_right_comm (Multiset.prod (normalizedFactors a)) ua (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit,
h1 ub.isUnit, h1 ua.isUnit, ← mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
congr
rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id, Finset.prod_multiset_map_count,
Finset.prod_multiset_map_count,
Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ← Finset.prod_mul_distrib]
· simp_rw [id, ← pow_add, this]
all_goals simp only [Multiset.mem_toFinset]
· intro p _ hpb
simp [hpb]
· intro p _ hpa
simp [hpa]
refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp
all_goals simp only [Multiset.mem_toFinset, Finset.mem_union]
· rintro p (hpa | hpb) <;> apply prime_of_normalized_factor <;> assumption
·
rintro p (hp | hp) q (hq | hq) hdvd <;>
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq] <;>
exact
normalize_eq_normalize hdvd
((prime_of_normalized_factor _ hp).irreducible.dvd_symm (prime_of_normalized_factor _ hq).irreducible hdvd)
