natCast_gcdA_mul_intCast_eq_gcd

Mathlib.Algebra.CharP.Invertible

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

← MathLib Explorer

English

For any natural n, in a ring R with CharP p, we have (gcdA(p) * n) cast to R equals gcd(n,p) cast to R.

Русский

Для любого натурального n в кольце R с CharP p имеем (gcdA(p) · n)⟪R⟫ = gcd(n,p)⟪R⟫.

LaTeX

$$$(n.gcdA p * n : R) = n.gcd p$$$

Lean4

theorem natCast_gcdA_mul_intCast_eq_gcd (n : ℕ) : (n.gcdA p * n : R) = n.gcd p :=
  Nat.commute_cast _ _ |>.eq.trans <| CharP.intCast_mul_natCast_gcdA_eq_gcd n

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

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

Разделы

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

Аффилиация

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