equivQuotientZPowOfEquiv_symm — Mathlib

English

The inverse of the quotient equivalence induced by an isomorphism e is the quotient equivalence induced by the inverse isomorphism e^{-1}.

Русский

Обратное к эквивалентности по изоморфизму e есть эквивалентность по обратному изоморфизму e^{-1}.

LaTeX

$$$(\\mathrm{equivQuotientZPowOfEquiv}\,e\,n)^{-1} = \\mathrm{equivQuotientZPowOfEquiv}\,e^{-1}\,n$$$

Lean4

@[to_additive (attr := simp)]
theorem equivQuotientZPowOfEquiv_symm : (equivQuotientZPowOfEquiv e n).symm = equivQuotientZPowOfEquiv e.symm n :=
  rfl

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