discr — Mathlib

English

Given an A-algebra B and a finite index set ι, define discr A b as the determinant of the trace matrix traceMatrix A b.

Русский

Для кольца A и алгебры B над A с конечной основой ι дискриминант равен детерминанту матрицы следа traceMatrix A b.

LaTeX

$$discr A b = (traceMatrix A b).det$$

Lean4

/-- Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define
`discr A ι b` as the determinant of `traceMatrix A ι b`. -/
noncomputable def discr (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) :=
  (traceMatrix A b).det

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