inl_mul_inr_eq_mk_of_unit — Mathlib

English

For unit elements m ∈ G₀ˣ and n ∈ H₀ˣ, the product inl(m) · inr(n) corresponds to the pair (m, n).

Русский

Для единиц m ∈ G₀ˣ и n ∈ H₀ˣ произведение inl(m) и inr(n) соответствует паре (m, n).

LaTeX

$$$(\mathrm{inl}\ G_0\ H_0\ m) * (\mathrm{inr}\ G_0\ H_0\ n) = (m, n)$$$

Lean4

theorem inl_mul_inr_eq_mk_of_unit (m : G₀ˣ) (n : H₀ˣ) : (inl G₀ H₀ m * inr G₀ H₀ n) = (m, n) := by
  simp [inl, WithZero.withZeroUnitsEquiv, inr, ← WithZero.coe_mul]

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