instPowQuotientNat — Mathlib

English

The nsmul construction on the quotient is equal to the explicit definition by the map used in the quotient.

Русский

Конструкция nsmul на факторе совпадает с явным определением через отображение в факторе.

LaTeX

$$$AddCon.Quotient.nsmul\\, c = \\text{defined via } Quotient.map' (n \\cdot)\\;\\dots$$$

Lean4

@[to_additive existing AddCon.Quotient.nsmul]
instance {M : Type*} [Monoid M] (c : Con M) : Pow c.Quotient ℕ where
  pow x n := Quotient.map' (fun x => x ^ n) (fun _ _ => c.pow n) x

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