discr_def

Mathlib.RingTheory.Discriminant

URI: https://scilib.ai/kg/mathlib#Algebra.discr_def

English

The discriminant is invariant under algebra isomorphisms: discr A b = discr A (f ∘ b) for any algebra isomorphism f.

Русский

Дискриминант сохраняется при изоморфизма алгебр: discr A b = discr A (f ∘ b).

LaTeX

$$discr A b = discr A (f \\circ b)$$

Lean4

theorem discr_def [Fintype ι] (b : ι → B) : discr A b = (traceMatrix A b).det :=
  rfl

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

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

Разделы

Аффилиация

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