sigmaCongrRight_mul — Mathlib

English

For F,G ∶ ∀ a, Perm (β a), the right-congruence sigmaCongrRight satisfies sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G).

Русский

Для F,G : ∀ a, Perm (β a) справедливо sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G).

LaTeX

$$$$sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G).$$$$

Lean4

@[simp]
theorem sigmaCongrRight_mul {α : Type*} {β : α → Type*} (F : ∀ a, Perm (β a)) (G : ∀ a, Perm (β a)) :
    sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G) :=
  rfl

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