commute_inl_inr — Mathlib

English

Any left-injection element and right-injection element commute in the product.

Русский

Любые элементы inl(m) и inr(n) коммутируют в произведении.

LaTeX

$$∀ m∈G_0, n∈H_0, Commute( (\mathrm{inl}\ G_0\ H_0 m), (\mathrm{inr}\ G_0\ H_0 n) )$$

Lean4

theorem commute_inl_inr (m : G₀) (n : H₀) : Commute (inl G₀ H₀ m) (inr G₀ H₀ n) := by
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit m <;>
      obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit n <;>
    simp [inl, inr, WithZero.withZeroUnitsEquiv, commute_iff_eq, ← WithZero.coe_mul]

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