isAssociative_right — Mathlib

English

If ga is associative and f is surjective and f semiconjugates ga to gb, then gb is associative.

Русский

Если ga ассоциативна, а f сюръективна и полуприводит ga к gb, то gb ассоциативна.

LaTeX

$$$ \forall x,y,z,\ gb( gb(x,y), z) = gb(x, gb(y,z)) $$$

Lean4

theorem isAssociative_right [Std.Associative ga] (h : Semiconj₂ f ga gb) (h_surj : Surjective f) : Std.Associative gb :=
  ⟨h_surj.forall₃.2 fun x₁ x₂ x₃ ↦ by simp only [← h.eq, Std.Associative.assoc (op := ga)]⟩

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