AbsoluteValue

📁 Source: Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

Statistics

Metric	Count
Definitions	0
Theorems det_le, det_sum_le, det_sum_smul_le	3
Total	3

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring AbsoluteValue.funLike	det AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.factorial Fintype.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	det_apply AbsoluteValue.sum_le IsStrictOrderedRing.toIsOrderedRing Finset.sum_congr AbsoluteValue.map_units_int_smul AbsoluteValue.map_prod Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.prod_le_prod IsStrictOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono NonnegHomClass.apply_nonneg AbsoluteValue.nonnegHomClass Finset.prod_const Finset.sum_const Fintype.card_perm nsmul_eq_mul
det_sum_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring AbsoluteValue.funLike	det Finset.sum Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.factorial Fintype.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.card	—	det_le sum_apply AbsoluteValue.sum_le IsStrictOrderedRing.toIsOrderedRing Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.sum_const
det_sum_smul_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring AbsoluteValue.funLike	det Finset.sum Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing smul Algebra.toSMul Algebra.id AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.factorial Fintype.card Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finset.card	—	smul_mul_assoc IsScalarTower.right det_sum_le AbsoluteValue.map_mul mul_le_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toMulPosMono AbsoluteValue.nonneg LE.le.trans

---

← Back to Index