Theorems · Theorem · commutative algebra

Algebra.discr_of_matrix_mulVec

∀ {A : Type u} {B : Type v} {ι : Type w} [inst : DecidableEq ι] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Fintype ι] (b : ι → B) (P : Matrix ι ι A),
  Algebra.discr A ((P.map ⇑(algebraMap A B)).mulVec b) = P.det ^ 2 * Algebra.discr A b

Relation between Algebra.discr A ι b and Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b).

Defined in

Mathlib.RingTheory.Discriminant

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqCommRingCommRingAlgebraFintype