quotientEquivOfEq_mk — Mathlib

English

If h is an equality of subgroups, then the quotient equivalence applied to mk a equals mk a for any a.

Русский

Если h: s = t, то применённое к mk a отображение эквивалентности даёт mk a.

LaTeX

$$$\text{quotientEquivOfEq} \, h \, (\text{QuotientGroup.mk } a) = \text{QuotientGroup.mk } a$$$

Lean4

theorem quotientEquivOfEq_mk (h : s = t) (a : α) : quotientEquivOfEq h (QuotientGroup.mk a) = QuotientGroup.mk a :=
  rfl

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