map_surjective

Mathlib.RingTheory.WittVector.Basic

URI: https://scilib.ai/kg/mathlib#WittVector.map_surjective

English

The Witt vector map induced by a surjective ring homomorphism is surjective.

Русский

Отображение WittVector, получаемое из сюръективного гомоморфизма кольца, сюръективно.

LaTeX

$$$\\text{map_surjective }(f,hf) : (\\mathrm{map}\\, f) \\text{ Surjective}$$$

Lean4

theorem map_surjective (f : R →+* S) (hf : Surjective f) : Surjective (map f : 𝕎 R → 𝕎 S) :=
  mapFun.surjective f hf

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

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

Разделы

Аффилиация

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