exists_eq_mul_inl — Mathlib

English

There exists n ∈ N such that (GroupExtension.Section.instFunLike S).coe σ g = (instHMul.hMul (S.inl n) ((GroupExtension.Section.instFunLike S).coe σ' g)).

Русский

Существует n ∈ N такое, что сопоставление σ g равно произведению σ' g и S.inl n.

LaTeX

$$$ \\exists n:\\,N, \\ σ(g) = σ'(g) \\cdot S.inl n $$$

Lean4

@[to_additive]
theorem exists_eq_mul_inl : ∃ n : N, σ g = σ' g * S.inl n :=
  by
  obtain ⟨n, hn⟩ := inv_mul_mem_range_inl σ' σ g
  exact ⟨n, by rw [hn, mul_inv_cancel_left]⟩

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