exists_mul_eq_inl_mul_mul — Mathlib

English

There exists n ∈ N such that σ(g₁ g₂) = S.inl n · σ g₁ · σ g₂.

Русский

Существует n ∈ N такое, что σ(g₁ g₂) = S.inl n · σ g₁ · σ g₂.

LaTeX

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

Lean4

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

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