English
If a certain commuting condition holds, then applying the equivalence to a factor in normalizedFactors(a) matches applying the monoid equivalence to the factor p.
Русский
При выполнении условия совместимости нормализации и эквивалентности элемент-из фактора переходит согласованно через эквивалентность.
LaTeX
$$normalizedFactorsEquiv_apply (he) {a} {p} (hp) : normalizedFactorsEquiv he a ⟨p, hp⟩ = f p$$
Lean4
theorem dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y :=
by
constructor
· rintro ⟨_, c, hc, rfl⟩
simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff, lt_add_iff_pos_right,
normalizedFactors_pos, hc]
· intro h
exact
dvdNotUnit_of_dvd_of_not_dvd ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
(mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)
