coe_neg

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#SignType.coe_neg

English

Coercion preserves negation: (↑(-s) : α) = -↑s.

Русский

Приведение к равенству сохраняет отрицание: ↑(-s) = -↑s.

LaTeX

$$$\uparrow(-s) = - \uparrow s$$$

Lean4

@[simp, norm_cast]
theorem coe_neg {α : Type*} [One α] [SubtractionMonoid α] (s : SignType) : (↑(-s) : α) = -↑s := by cases s <;> simp

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

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

Разделы

Аффилиация

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