Determinant

📁 Source: Mathlib/LinearAlgebra/Complex/Determinant.lean

Statistics

Metric	Count
Definitions	0
Theorems det_conjAe, linearEquiv_det_conjAe	2
Total	2

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_conjAe 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring Complex AddCommGroup.toAddCommMonoid addCommGroup Algebra.toModule Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det AlgEquiv.toLinearMap conjAe Real.instNeg Real.instOne	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix toMatrix_conjAe Matrix.det_fin_two_of mul_neg mul_one MulZeroClass.mul_zero sub_zero
linearEquiv_det_conjAe 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv Real CommSemiring.toSemiring CommRing.toCommSemiring Real.commRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Complex AddCommGroup.toAddCommMonoid addCommGroup Algebra.toModule Real.instCommSemiring instSemiring Algebra.complexToReal Algebra.id instCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det AlgEquiv.toLinearEquiv conjAe Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.instOne	—	RingHomInvPair.ids LinearEquiv.coe_det AlgEquiv.toLinearEquiv_toLinearMap det_conjAe Units.coe_neg_one

---

← Back to Index