quotientEquivAlgOfEq_symm — Mathlib

English

The inverse of quotientEquivAlgOfEq is itself the quotientEquivAlgOfEq with the symmetric equality h.symm.

Русский

Обратное отображение quotientEquivAlgOfEq равно quotientEquivAlgOfEq с симметричным равенством h.symm.

LaTeX

$$$\\left(\\text{quotientEquivAlgOfEq } R \\_ h\\right)^{-1} = \\text{quotientEquivAlgOfEq } R \\_ h^{\\mathrm{symm}}$$$

Lean4

@[simp]
theorem quotientEquivAlgOfEq_symm {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :
    (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ h.symm :=
  by
  ext
  rfl

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