English
Given h' : A' = B' and h : A = B, there is an isomorphism A/(A' ⊓ A) ≃* B/(B' ⊓ B).
Русский
Пусть h' : A' = B' и h : A = B; существует изоморфизм A/(A' ⊓ A) ≃* B/(B' ⊓ B).
LaTeX
$$equivQuotientSubgroupOfOfEq {A' A B' B} [hAN] [hBN] (h' : A' = B') (h : A = B) : A ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B$$
Lean4
/-- Let `A', A, B', B` be subgroups of `G`.
If `A' = B'` and `A = B`, then the quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic.
Applying this equiv is nicer than rewriting along the equalities, since the type of
`(A'.subgroupOf A : Subgroup A)` depends on `A`.
-/
@[to_additive /-- Let `A', A, B', B` be subgroups of `G`. If `A' = B'` and `A = B`, then the
quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic. Applying this equiv is nicer than
rewriting along the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends on
`A`. -/
]
def equivQuotientSubgroupOfOfEq {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal]
[hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) : A ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B :=
(quotientMapSubgroupOfOfLe h'.le h.le).toMulEquiv (quotientMapSubgroupOfOfLe h'.ge h.ge) (by ext ⟨x, hx⟩; rfl)
(by ext ⟨x, hx⟩; rfl)
