coe_iterateFrobenius_mul

Mathlib.Algebra.CharP.Frobenius

URI: https://scilib.ai/kg/mathlib#coe_iterateFrobenius_mul

English

Frobenius fixes natural numbers embedded into R via natCast: frobenius R p n = n for all n ∈ ℕ.

Русский

Фробениус фиксирует натуральные числа, встроенные через natCast: frobenius R p n = n.

LaTeX

$$$\forall n \in \mathbb{N},\ frobenius R p n = n$$$

Lean4

theorem coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n] :=
  funext (iterateFrobenius_mul_apply R p m n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru