English
For monoids M,N, two elements x=(x1,x2) and z=(z1,z2) of M×N are associated if and only if x1 is associated to z1 and x2 is associated to z2.
Русский
В парах М×N два элемента ассоциированы тогда и только тогда, когда соответствующие координаты ассоциированы друг с другом.
LaTeX
$$$(x_1,x_2) \\sim_u (z_1,z_2) \\;\\iff\\; x_1 \\sim_u z_1 \\;\\wedge\\; x_2 \\sim_u z_2$$$
Lean4
theorem associated_iff {M N : Type*} [Monoid M] [Monoid N] {x z : M × N} : x ~ᵤ z ↔ x.1 ~ᵤ z.1 ∧ x.2 ~ᵤ z.2 :=
⟨fun ⟨u, hu⟩ =>
⟨⟨(MulEquiv.prodUnits.toFun u).1, (Prod.eq_iff_fst_eq_snd_eq.1 hu).1⟩,
⟨(MulEquiv.prodUnits.toFun u).2, (Prod.eq_iff_fst_eq_snd_eq.1 hu).2⟩⟩,
fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ => ⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩
