equivQuotientZPowOfEquiv_refl — Mathlib

English

The z-power quotient equivalence corresponding to a identity isomorphism is the identity, i.e., the equivalence with e = Refl_A yields the trivial quotient isomorphism.

Русский

Эквивалентность по z-пowers, соответствующая тождественному изоморфизму, является тождественной.

LaTeX

$$$\\text{equivQuotientZPowOfEquiv}(\\mathrm{MulEquiv.refl}\\,A, n) = \\mathrm{id}$$$

Lean4

@[to_additive (attr := simp)]
theorem equivQuotientZPowOfEquiv_refl :
    MulEquiv.refl (A ⧸ (zpowGroupHom n : A →* A).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n :=
  by
  ext x
  rw [← Quotient.out_eq' x]
  rfl

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