zpowinst — Mathlib

English

Integer powers on quotient are defined by a canonical instance mapping.

Русский

Целочисленные степени на факторе задаются каноническим отображением.

LaTeX

$$$\\text{Pow } c.Quotient \\mathbb{Z}$ defined by $x^n$ via quotient map$$

Lean4

/-- The integer power induced on the quotient by a congruence relation on a type with a
division. -/
@[to_additive existing AddCon.Quotient.zsmul]
instance zpowinst : Pow c.Quotient ℤ :=
  ⟨fun x z => Quotient.map' (fun x => x ^ z) (fun _ _ h => c.zpow z h) x⟩

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