exists_mul_eq_mul_mul_inl — Mathlib

English

There exists n ∈ N such that σ(g₁ g₂) = σ g₁ · σ g₂ · S.inl n, i.e., the discrepancy between σ(g₁ g₂) and σ(g₁)σ(g₂) lies in the image of S.inl.

Русский

Существует n ∈ N такое, что σ(g₁ g₂) = σ g₁ · σ g₂ · S.inl n, то есть расхождение σ(g₁ g₂) и σ(g₁)σ(g₂) лежит в образе S.inl.

LaTeX

$$$ \\exists n:\\,N, \\ σ(g_1 g_2) = σ(g_1) \\cdot σ(g_2) \\cdot S.inl(n) $$$

Lean4

@[to_additive]
theorem exists_mul_eq_mul_mul_inl : ∃ n : N, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n :=
  by
  obtain ⟨n, hn⟩ := mul_inv_mul_mul_mem_range_inl σ g₁ g₂
  use n⁻¹
  rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]

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