castHom_apply

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.castHom_apply

← MathLib Explorer

English

The canonical castHom applied to i equals cast i.

Русский

Применение castHom к i даёт cast i.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} {R : Type*} [Ring R] {m : \\\\mathbb{N}} [CharP R m] (i : ZMod n), \\\\operatorname{castHom} h R i = \\\\operatorname{cast} i$$$

Lean4

@[simp]
theorem castHom_apply {h : m ∣ n} (i : ZMod n) : castHom h R i = cast i :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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