quotientMulEquivOfEq — Mathlib

English

The mk function respects equality of subgroups, giving a canonical isomorphism when subgroups coincide.

Русский

Функция mk уважает равенство подгрупп, давая канонический изоморфизм при совпадении подгрупп.

LaTeX

$$QuotientGroup.quotientMulEquivOfEq h (QuotientGroup.mk x) = QuotientGroup.mk x$$

Lean4

/-- If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
isomorphic. -/
@[to_additive /-- If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
    isomorphic. -/
    ]
def quotientMulEquivOfEq {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N :=
  { Subgroup.quotientEquivOfEq h with map_mul' := fun q r => Quotient.inductionOn₂' q r fun _g _h => rfl }

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