Theorems · Theorem · linear algebra

LinearMap.det_map

∀ {K : Type u_5} {V : Type u_6} {W : Type u_7} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup W] [inst_4 : Module K W] {F : Type u_8}
  [inst_5 : EquivLike F (Module.End K V) (Module.End K W)] [AlgEquivClass F K (Module.End K V) (Module.End K W)] (f : F)
  (x : Module.End K V), LinearMap.det (f x) = LinearMap.det x

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleAddCommGroupModuleEquivLikeAlgEquivClass