congr_mk — Mathlib

English

If e is a MulEquiv G H sending G' to H', then the induced congruence on quotients takes mk x to e x after mapping.

Русский

Если e — мультиэквивариант G к H переводит G' в H', то индуцированное отображение фактор-групп переводит mk x в e x.

LaTeX

$$$\\text{congr } G' H' e \\; (\\mathrm{mk}\_{} x) = \\mathrm{mk'}(e x)$$$

Lean4

@[simp]
theorem congr_mk (e : G ≃* H) (he : G'.map ↑e = H') (x) : congr G' H' e he (mk x) = e x :=
  rfl

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