English
Given the commuting hypothesis, evaluating the equivalence on a factor yields the image under f.
Русский
При заданном условии совместимости, применение эквивалентности к фактору даёт образ через f.
LaTeX
$$normalizedFactorsEquiv_apply (he) {a} {p} (hp) : normalizedFactorsEquiv he a ⟨p, hp⟩ = f p$$
Lean4
/-- Noncomputably defines a `normalizationMonoid` structure on a `UniqueFactorizationMonoid`. -/
protected noncomputable def normalizationMonoid : NormalizationMonoid α :=
normalizationMonoidOfMonoidHomRightInverse
{ toFun := fun a : Associates α =>
if a = 0 then 0
else ((normalizedFactors a).map (Classical.choose mk_surjective.hasRightInverse : Associates α → α)).prod
map_one' := by nontriviality α; simp
map_mul' := fun x y => by
by_cases hx : x = 0
· simp [hx]
by_cases hy : y = 0
· simp [hy]
simp [hx, hy] }
(by
intro x
dsimp
by_cases hx : x = 0
· simp [hx]
have h :
Associates.mkMonoidHom ∘ Classical.choose mk_surjective.hasRightInverse = (id : Associates α → Associates α) :=
by
ext x
rw [Function.comp_apply, mkMonoidHom_apply, Classical.choose_spec mk_surjective.hasRightInverse x]
rfl
rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ← associated_iff_eq]
apply prod_normalizedFactors hx)
