coe_ofNat — Mathlib

English

For a natural number n, the germ of OfNat n coincides with the canonical OfNat embedding of n into germs.

Русский

Для натурального числа n жерма OfNat n совпадает с каноническим вложением n в жермы.

LaTeX

$$$[Pow G M] \\; (f : \\alpha \\to G) \\; (n : \\mathbb{N}) \\Rightarrow \\uparrow(f)^{n} = (\\uparrow f)^{n}.$$$

Lean4

@[simp, norm_cast]
theorem coe_ofNat [NatCast M] (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : α → M) : Germ l M) = OfNat.ofNat n :=
  rfl

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