mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle

English

In a pi-group with a commutative monoid M, the equality (mulSingle k u) · (mulSingle l v) = (mulSingle m u) · (mulSingle n v) holds iff one of the following: k = m and l = n; or u = v and k = n and l = m; or u v = 1 and k = l and m = n, given u,v ≠ 1.

Русский

В произведении индексов Pi-группа с коммутативным моноидом M равенство (mulSingle k u)·(mulSingle l v) = (mulSingle m u)·(mulSingle n v) эквивалентно одному из трёх условий: k=m и l=n; или u=v и k=n и l=m; или uv=1 и k=l и m=n, при условиях u ≠ 1, v ≠ 1.

LaTeX

$$$\left(\mathrm{mulSingle}_k u\right) \left(\mathrm{mulSingle}_l v\right) = \left(\mathrm{mulSingle}_m u\right) \left(\mathrm{mulSingle}_n v\right) \;\iff\; (k=m \land l=n) \lor (u=v \land k=n \land l=m) \lor (u v = 1 \land k=l \land m=n) \\text{for } u,v \neq 1$$$

Lean4

@[to_additive]
theorem mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {M : Type*} [CommMonoid M] {k l m n : I} {u v : M}
    (hu : u ≠ 1) (hv : v ≠ 1) :
    (mulSingle k u : I → M) * mulSingle l v = mulSingle m u * mulSingle n v ↔
      k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · have hk := congr_fun h k
    have hl := congr_fun h l
    have hm := (congr_fun h m).symm
    have hn := (congr_fun h n).symm
    simp only [mul_apply, mulSingle_apply] at hk hl hm hn
    rcases eq_or_ne k m with (rfl | hkm)
    · refine Or.inl ⟨rfl, not_ne_iff.mp fun hln => (hv ?_).elim⟩
      rcases eq_or_ne k l with (rfl | hkl)
      · rwa [if_neg hln.symm, if_neg hln.symm, one_mul, one_mul] at hn
      · rwa [if_neg hkl.symm, if_neg hln, one_mul, one_mul] at hl
    · rcases eq_or_ne m n with (rfl | hmn)
      · rcases eq_or_ne k l with (rfl | hkl)
        · rw [if_neg hkm.symm, if_neg hkm.symm, one_mul, if_pos rfl] at hm
          exact Or.inr (Or.inr ⟨hm, rfl, rfl⟩)
        · simp only [if_neg hkm, if_neg hkl, mul_one] at hk
          dsimp at hk
          contradiction
      · rw [if_neg hkm.symm, if_neg hmn, one_mul, mul_one] at hm
        obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hm.symm hu)).1
        rw [if_neg hkm, if_neg hkm, one_mul, mul_one] at hk
        obtain rfl := (ite_ne_right_iff.mp (ne_of_eq_of_ne hk.symm hu)).1
        exact Or.inr (Or.inl ⟨hk.trans (if_pos rfl), rfl, rfl⟩)
  · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl, rfl⟩ | ⟨h, rfl, rfl⟩)
    · rfl
    · apply mul_comm
    · simp_rw [← Pi.mulSingle_mul, h, mulSingle_one]

Похожие утверждения