coe_mkUnit

Mathlib.RingTheory.WittVector.DiscreteValuationRing

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

English

If A is a Witt vector with A.coeff 0 = a (a unit), then the constructed unit mkUnit hA in 𝕎 k equals A.

Русский

Если A — Witt-вектор с A.coeff 0 = a (единица), то сконструированная единица mkUnit hA равна A.

LaTeX

$$@[simp] mkUnit_coe: (mkUnit hA : 𝕎 k) = A$$

Lean4

@[simp]
theorem coe_mkUnit {a : Units k} {A : 𝕎 k} (hA : A.coeff 0 = a) : (mkUnit hA : 𝕎 k) = A :=
  rfl

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

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

Разделы

Аффилиация

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