discrim_neg

Mathlib.Algebra.QuadraticDiscriminant

URI: https://scilib.ai/kg/mathlib#discrim_neg

English

discrim(-a,-b,-c) = discrim(a,b,c).

Русский

Дискриминант при изменении знаков на (-a,-b,-c) равен дискриминанту.

LaTeX

$$$\mathrm{discrim}(-a,-b,-c) = \mathrm{discrim}(a,b,c)$$$

Lean4

@[simp]
theorem discrim_neg [Ring R] (a b c : R) : discrim (-a) (-b) (-c) = discrim a b c := by simp [discrim]

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

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

Разделы

Аффилиация

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