congr

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.congr

English

If p = q, then CharP R q holds given CharP R p.

Русский

Если p = q, тогда CharP R q возникает из CharP R p.

LaTeX

$$$(p = q) \Rightarrow CharP(R, q).$$$

Lean4

theorem congr {q : ℕ} (h : p = q) : CharP R q :=
  h ▸ ‹CharP R p›

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

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

Разделы

Аффилиация

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