Determinant

📁 Source: Mathlib/Topology/Algebra/Module/Determinant.lean

Statistics

Metric	Count
Definitions det	1
Theorems det_coe_symm, det_one_smulRight, det_pi, det_smulRight, det_toSpanSingleton	5
Total	6

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_coe_symm 📖	mathematical	—	ContinuousLinearMap.det EuclideanDomain.toCommRing Field.toEuclideanDomain toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid symm InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	RingHomInvPair.ids LinearEquiv.det_coe_symm

ContinuousLinearMap

Definitions

Name	Category	Theorems
det 📖	CompOp	30 math math: LinearMap.det_toContinuousLinearMap, continuous_det, MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, det_fderivPolarCoordSymm, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, det_pi, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux1, MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, det_toSpanSingleton, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2, MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul, ContinuousLinearEquiv.det_coe_symm, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, det_one_smulRight, det_fderivPiPolarCoordSymm, MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin, det_smulRight, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_one_smulRight 📖	mathematical	—	det Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring toSpanSingleton NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero	—	det_toSpanSingleton
det_pi 📖	mathematical	—	det Pi.topologicalSpace Pi.addCommGroup Pi.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid pi Pi.addCommMonoid comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids proj Finset.prod CommRing.toCommMonoid Finset.univ	—	LinearMap.det_pi
det_smulRight 📖	mathematical	—	det Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring smulRight NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Algebra.id ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring funLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsScalarTower.right ContinuousMul.to_continuousSMul LinearMap.det_ring
det_toSpanSingleton 📖	mathematical	—	det Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring toSpanSingleton NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero	—	ContinuousMul.to_continuousSMul IsScalarTower.left smulRight_id IsScalarTower.right det_smulRight one_mul

---

← Back to Index