English
Two subalgebras that are equal are equivalent as algebras; i.e., if S = T, there is a canonical R-algebra isomorphism S ≃ₐ[R] T given by equality.
Русский
Две равные по смыслу подалгебры эквивалентны как алгебры; если S = T, существует каноническое отрасление S ≃ₐ[R] T, порожденное равенством.
LaTeX
$$$S = T \Rightarrow S \cong_R T$ via $\text{equivOfEq}(S,T,\,h)$, where $h$ is the equality.$$
Lean4
/-- Two subalgebras that are equal are also equivalent as algebras.
This is the `Subalgebra` version of `LinearEquiv.ofEq` and `Equiv.setCongr`. -/
@[simps apply]
def equivOfEq (S T : Subalgebra R A) (h : S = T) : S ≃ₐ[R] T
where
__ := LinearEquiv.ofEq _ _ (congr_arg toSubmodule h)
toFun x := ⟨x, h ▸ x.2⟩
invFun x := ⟨x, h.symm ▸ x.2⟩
map_mul' _ _ := rfl
commutes' _ := rfl
