English
If emultiplicity equality holds for p, m, n under a factor orderIso, then the equality persists under symmetries d and d.symm.
Русский
Если равенство эмпемлипти сохраняется под образами d и d.symm, то равенство сохраняется и под исходными множествами.
LaTeX
$$emultiplicity p m = emultiplicity p' n$$
Lean4
/-- The order isomorphism between the factors of `mk m` and the factors of `mk n` induced by a
bijection between the factors of `m` and the factors of `n` that preserves `∣`. -/
@[simps]
def mkFactorOrderIsoOfFactorDvdEquiv {m : M} {n : N} {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }}
(hd : ∀ l l', (d l : N) ∣ d l' ↔ (l : M) ∣ (l' : M)) : Set.Iic (Associates.mk m) ≃o Set.Iic (Associates.mk n)
where
toFun
l :=
⟨Associates.mk
(d
⟨associatesEquivOfUniqueUnits ↑l, by
obtain ⟨x, hx⟩ := l
rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
exact hx⟩),
mk_le_mk_iff_dvd.mpr (Subtype.prop (d ⟨associatesEquivOfUniqueUnits ↑l, _⟩))⟩
invFun
l :=
⟨Associates.mk
(d.symm
⟨associatesEquivOfUniqueUnits ↑l, by
obtain ⟨x, hx⟩ := l
rw [Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_dvd_iff]
exact hx⟩),
mk_le_mk_iff_dvd.mpr (Subtype.prop (d.symm ⟨associatesEquivOfUniqueUnits ↑l, _⟩))⟩
left_inv := fun ⟨l, hl⟩ => by
simp only [Subtype.coe_eta, Equiv.symm_apply_apply, Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, mk_out,
out_mk, normalize_eq]
right_inv := fun ⟨l, hl⟩ => by
simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_mk, associatesEquivOfUniqueUnits_apply, out_mk,
normalize_eq, mk_out]
map_rel_iff' := by
rintro ⟨a, ha⟩ ⟨b, hb⟩
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Associates.mk_le_mk_iff_dvd, hd, associatesEquivOfUniqueUnits_apply,
out_dvd_iff, mk_out]
