hom_C

Mathlib.Algebra.MvPolynomial.CommRing

URI: https://scilib.ai/kg/mathlib#MvPolynomial.hom_C

English

For any ring homomorphism f from MvPolynomial σ ℤ to S and any integer n, f(C n) = n in S.

Русский

Для любого кольцевого гомоморфизма f: MvPolynomial σ ℤ →+* S и любого целого числа n выполняется f(C n) = n в S.

LaTeX

$$$f(C\\;n) = (n : S)$$$

Lean4

theorem hom_C (f : MvPolynomial σ ℤ →+* S) (n : ℤ) : f (C n) = (n : S) :=
  eq_intCast (f.comp C) n

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

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

Разделы

Аффилиация

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