Determinant

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

Statistics

Metric	Count
Definitions	0
Theorems det_zero''	1
Total	1

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_zero'' 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim det_zero Module.finrank_subsingleton pow_one det_zero' Finite.of_fintype Module.Basis.index_nonempty

---

← Back to Index