single_inv_ρ_self_add_single_mem_boundaries₁

English

For any g ∈ G and a ∈ A, the element single g⁻¹ (ρ g⁻¹ a) + single g a lies in B1(G,A).

Русский

Для любых g ∈ G и a ∈ A элемент single g⁻¹ (ρ g⁻¹ a) + single g a принадлежит B1(G,A).

LaTeX

$$single g⁻¹ (A.ρ g⁻¹ a) + single g a ∈ B_1(G,A)$$

Lean4

theorem single_inv_ρ_self_add_single_mem_boundaries₁ (g : G) (a : A) :
    single g⁻¹ (A.ρ g⁻¹ a) + single g a ∈ boundaries₁ A :=
  by
  rw [← d₂₁_single_inv_mul_ρ_add_single g 1]
  exact Set.mem_range_self _

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